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  6499  genpmu  6500  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  nqprloc  6527  appdivnq  6543  appdiv0nq  6544  mulnqprl  6548  mulnqpru  6549  distrlem1prl  6557  distrlem1pru  6558  ltprordil  6564  1idprl  6565  1idpru  6566  ltexprlemrl  6583  ltexprlemru  6585  ltexpri  6586  addcanprleml  6587  addcanprlemu  6588  recexprlem1ssl  6604  recexpr  6609  aptiprlemu  6611  archpr  6614  cauappcvgprlemopl  6617  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  0idsr  6675  1idsr  6676  recexsrlem  6682  addgt0sr  6683  axarch  6753  cnegexlem1  6963  cnegex  6966  negeu  6979  pncan  6994  pncan3  6996  npcan  6997  mulneg1  7168  ltnegcon2  7234  add20  7244  subge0  7245  lesub0  7249  reapval  7340  recexre  7342  apreap  7351  ltmul1a  7355  reapneg  7361  cru  7366  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  apti  7386  gt0ap0  7388  recexap  7396  rerecclap  7468  recgt0  7577  prodgt0gt0  7578  lemul1a  7585  lemul12a  7589  lt2msq  7613  ltrec1  7615  recreclt  7627  creui  7673  cju  7674  avglt2  7921  un0addcl  7971  nn0ge2m1nn  7998  nn0nndivcl  8000  elnn0z  8014  peano2z  8037  elz2  8068  peano5uzti  8102  zindd  8112  eluzadd  8257  nn0pzuz  8286  eluz2b2  8296  eqreznegel  8305  nn0ge2m1nnALT  8309  divfnzn  8312  qmulz  8314  qapne  8330  qreccl  8331  cnref1o  8337  ge0p1rp  8369  xrltso  8467  z2ge  8489  xltnegi  8498  ixxssixx  8521  lincmb01cmp  8621  iccf1o  8622  fztri3or  8653  fzdcel  8654  fznlem  8655  fzn  8656  uzsubsubfz  8661  fzsplit2  8664  fzopth  8674  fzdifsuc  8693  fzrev2i  8698  elfz1b  8702  fzneuz  8713  fzrevral  8717  ige2m1fz  8722  elfz0ubfz0  8732  elfz0fzfz0  8733  4fvwrd4  8747  2ffzeq  8748  fzospliti  8782  fzosplit  8783  fzo1fzo0n0  8789  fzonmapblen  8793  fzoaddel  8798  fzosubel  8800  fzosubel3  8802  elfzodifsumelfzo  8807  elfzom1elp1fzo  8808  elfzom1p1elfzo  8820  elfzonelfzo  8836  peano2fzor  8838  frec2uzzd  8847  frec2uzuzd  8849  frec2uzrand  8852  frec2uzf1od  8853  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgfn  8859  frecuzrdgcl  8860  frecuzrdgsuc  8862  frecfzennn  8864  iseqfeq2  8886  expivallem  8890  expival  8891  expinnval  8892  expp1  8896  rpexpcl  8908  expaddzaplem  8932  leexp1a  8943  exple1  8944  subsq  8991  binom2  8995  binom3  8999  bernneq3  9004  expnbnd  9005  crre  9065  rereb  9071  cjreim2  9112  cjap  9114  sqrt0  9193  nn0abscl  9209  bj-omtrans  9390
  Copyright terms: Public domain W3C validator