ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpr Structured version   GIF version

Theorem simpr 103
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr ((φ ψ) → ψ)

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 100 1 ((φ ψ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-ia2 100
This theorem is referenced by:  simpri  106  simprd  107  imp  115  adantld  263  ibar  285  pm3.42  315  pm3.4  316  prth  326  sylancom  397  adantll  445  adantrl  447  adantlll  449  adantlrl  451  adantrll  453  adantrrl  455  simpllr  486  simplrr  488  simprlr  490  simprrr  492  anabs7  508  jcab  535  pm4.38  537  pm5.21  610  ioran  668  pm3.14  669  ordi  728  pm4.39  734  pm5.16  736  pm5.54dc  826  intnan  837  intnand  839  dcan  841  bimsc1  869  niabn  873  simp1r  928  simp2r  930  simp3r  932  3anandirs  1237  truanOLD  1260  bilukdc  1284  19.26  1367  exsimpr  1506  19.40  1519  cbvexh  1635  sbequilem  1716  spsbe  1720  cbvexdh  1798  euan  1953  moan  1966  datisi  2007  fresison  2015  rexex  2362  r19.26  2435  r19.40  2458  cbvraldva2  2531  cbvrexdva2  2532  gencbvex  2594  rspct  2643  rspcimdv  2651  rspcimedv  2652  rr19.28v  2677  elrab3t  2691  reu6  2724  rmob  2844  csbiebt  2880  rabssab  3021  ssddif  3165  difin  3168  difrab  3205  preqsn  3537  opprc2  3563  dfnfc2  3589  intmin4  3634  sndisj  3751  exss  3954  euotd  3982  suctr  4124  tfisi  4253  peano2  4261  relop  4429  releldm  4512  relelrn  4513  resiexg  4596  trin2  4659  xpmlem  4687  unielrel  4788  relcoi2  4791  iota2df  4834  iota2  4836  funopab4  4880  fun11uni  4912  imadiflem  4921  imain  4924  fneq12  4935  f1ssr  5041  fvelrnb  5164  ssimaex  5177  fvmpt2d  5200  fvmptdf  5201  dffo3  5257  ffvresb  5271  fmptco  5273  funfvima3  5335  f1imass  5356  fliftf  5382  fliftval  5383  riota2df  5431  riota5f  5435  acexmidlemcase  5450  ovprc2  5484  eloprabga  5533  eqfnov2  5550  ovmpt2dxf  5568  fnofval  5663  offval2  5668  ofrfval2  5669  caofinvl  5675  2ndrn  5751  1st2ndbr  5752  cnvf1o  5788  f1o2ndf1  5791  mpt2xopoveq  5796  sprmpt2  5798  dftpos4  5819  tpostpos  5820  tposf12  5825  dfsmo2  5843  smores  5848  tfrlem1  5864  tfrlem3ag  5865  tfrlem3a  5866  tfrlemisucaccv  5880  tfrlemi1  5887  tfrexlem  5889  rdgivallem  5908  frecabex  5923  frectfr  5924  frecrdg  5931  freccl  5932  oawordi  5988  nntri3  6014  nnaordi  6017  nnaordex  6036  nnawordex  6037  nnm00  6038  ersymb  6056  ertr  6057  erref  6062  iserd  6068  swoer  6070  erth  6086  iinerm  6114  erinxp  6116  ecinxp  6117  qsel  6119  qliftel  6122  qliftfun  6124  dom3  6192  ssdomg  6194  cnven  6224  dmaddpqlem  6361  nqpi  6362  mulcanenq  6369  ltaddnq  6390  ltexnqq  6391  prarloclemarch2  6402  ltrnqg  6403  enq0sym  6414  nqnq0pi  6420  nq0nn  6424  mulcanenq0ec  6427  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  prloc  6473  prarloclemlt  6475  prarloclemlo  6476  ltdfpr  6488  genplt2i  6492  genpml  6500  genpmu  6501  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  nqprloc  6528  appdivnq  6542  appdiv0nq  6543  mulnqprl  6547  mulnqpru  6548  distrlem1prl  6556  distrlem1pru  6557  ltprordil  6563  1idprl  6564  1idpru  6565  ltexprlemrl  6582  ltexprlemru  6584  ltexpri  6585  addcanprleml  6586  addcanprlemu  6587  recexprlem1ssl  6603  recexpr  6608  aptiprlemu  6610  archpr  6613  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  0idsr  6655  1idsr  6656  recexsrlem  6662  addgt0sr  6663  axarch  6733  cnegexlem1  6943  cnegex  6946  negeu  6959  pncan  6974  pncan3  6976  npcan  6977  mulneg1  7148  ltnegcon2  7214  add20  7224  subge0  7225  lesub0  7229  reapval  7320  recexre  7322  apreap  7331  ltmul1a  7335  reapneg  7341  cru  7346  apsym  7350  apcotr  7351  apadd1  7352  apneg  7355  mulext1  7356  apti  7366  gt0ap0  7368  recexap  7376  rerecclap  7448  recgt0  7557  prodgt0gt0  7558  lemul1a  7565  lemul12a  7569  lt2msq  7593  ltrec1  7595  recreclt  7607  creui  7653  cju  7654  avglt2  7901  un0addcl  7951  nn0ge2m1nn  7978  nn0nndivcl  7980  elnn0z  7994  peano2z  8017  elz2  8048  peano5uzti  8082  zindd  8092  eluzadd  8237  nn0pzuz  8266  eluz2b2  8276  eqreznegel  8285  nn0ge2m1nnALT  8289  divfnzn  8292  qmulz  8294  qapne  8310  qreccl  8311  cnref1o  8317  ge0p1rp  8349  xrltso  8447  z2ge  8469  xltnegi  8478  ixxssixx  8501  lincmb01cmp  8601  iccf1o  8602  fztri3or  8633  fzdcel  8634  fznlem  8635  fzn  8636  uzsubsubfz  8641  fzsplit2  8644  fzopth  8654  fzdifsuc  8673  fzrev2i  8678  elfz1b  8682  fzneuz  8693  fzrevral  8697  ige2m1fz  8702  elfz0ubfz0  8712  elfz0fzfz0  8713  4fvwrd4  8727  2ffzeq  8728  fzospliti  8762  fzosplit  8763  fzo1fzo0n0  8769  fzonmapblen  8773  fzoaddel  8778  fzosubel  8780  fzosubel3  8782  elfzodifsumelfzo  8787  elfzom1elp1fzo  8788  elfzom1p1elfzo  8800  elfzonelfzo  8816  peano2fzor  8818  frec2uzzd  8827  frec2uzuzd  8829  frec2uzrand  8832  frec2uzf1od  8833  frecuzrdgrrn  8835  frec2uzrdg  8836  frecuzrdgfn  8839  frecuzrdgcl  8840  frecuzrdgsuc  8842  frecfzennn  8844  iseqfeq2  8866  expivallem  8870  expival  8871  expinnval  8872  expp1  8876  rpexpcl  8888  expaddzaplem  8912  leexp1a  8923  exple1  8924  subsq  8971  binom2  8975  binom3  8979  bernneq3  8984  expnbnd  8985  crre  9045  rereb  9051  cjreim2  9092  cjap  9094  bj-omtrans  9344
  Copyright terms: Public domain W3C validator