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

Theorem simpl 106
Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpl ((𝜑𝜓) → 𝜑)

Proof of Theorem simpl
StepHypRef Expression
1 ax-ia1 103 1 ((𝜑𝜓) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-ia1 103
This theorem is referenced by:  simpli  108  simpld  109  imp  119  adantrd  268  iba  288  pm3.41  318  pm4.45im  321  prth  330  pm4.71  375  adantlr  454  adantrr  456  adantllr  458  adantlrr  460  adantrlr  462  adantrrr  464  simplll  493  simplrl  495  simprll  497  simprrl  499  anabs1  514  jcab  545  pm4.38  547  pm5.21  621  ioran  679  pm3.14  680  pm4.44  706  ordi  740  pm4.39  746  pm5.16  748  pm5.54dc  838  intnanr  850  intnanrd  852  dcan  853  dedlema  887  dedlemb  888  pm4.42r  889  prlem2  892  simp1l  939  simp2l  941  simp3l  943  3anandis  1253  xordc1  1300  anxordi  1307  falantru  1310  19.26  1386  exsimpl  1524  sbequ2  1668  sbcof2  1707  sbequilem  1735  sbequ8  1743  euan  1972  mooran1  1988  eupickbi  1998  2exeu  2008  dimatis  2033  rexim  2430  r19.26  2458  r19.40  2481  rr19.28v  2706  elrab3t  2720  eueq3dc  2738  mosubt  2741  reu6  2753  sbc2iegf  2856  sbcralt  2862  sbcrext  2863  rmob  2878  csbiebt  2914  ssab2  3052  difdif  3097  uneqin  3216  indifdir  3221  undif3ss  3226  rexm  3348  difsn  3529  opprc1  3599  unissel  3637  ssmin  3662  abssexg  3962  opelopabsb  4025  sess1  4102  ordelord  4146  onin  4151  suctr  4186  ordtriexmidlem  4273  ordtri2or2exmid  4324  tfi  4333  peano1  4345  peano2  4346  0nelxp  4400  0nelelxp  4401  brab2a  4421  mosubopt  4433  posng  4440  opabssxp  4442  ideqg  4515  relssres  4676  trin2  4744  dminss  4766  iota4an  4914  iota2  4921  fun11uni  4997  imadiflem  5006  funimaexg  5011  fneq12  5020  fvelrnb  5249  dffo4  5343  ffnfv  5351  ffvresb  5356  fmptco  5358  fcoconst  5362  fcof1  5451  isotr  5484  isopolem  5489  f1oiso  5493  acexmidlemcase  5535  ovprc1  5569  fnoprabg  5630  op1steq  5833  1stconst  5870  f1o2ndf1  5877  sprmpt2  5888  brtpos2  5897  tpostpos  5910  tposf12  5915  smores  5938  tfrlemi1  5977  freceq1  6010  freceq2  6011  frectfr  6016  omv2  6076  omsuc  6082  nnsucelsuc  6101  nntri3  6106  nnaordi  6112  nnmordi  6120  nnm00  6133  ecexr  6142  ertr  6152  swoer  6165  erth  6181  ecelqsdm  6207  iinerm  6209  ecinxp  6212  erovlem  6229  dom3  6287  phpelm  6359  nnwetri  6385  supubti  6405  supisoex  6413  ordiso2  6415  dmaddpqlem  6533  distrnqg  6543  ltanqi  6558  ltmnqi  6559  ltaddnq  6563  ltrnqg  6576  ltnnnq  6579  enq0sym  6588  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  distrnq0  6615  prarloclemn  6655  prarloc  6659  ltdfpr  6662  genplt2i  6666  addnqprl  6685  addnqpru  6686  nqprl  6707  appdivnq  6719  1idprl  6746  1idpru  6747  ltexpri  6769  recexpr  6794  cauappcvgprlemdisj  6807  archrecpr  6820  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  0idsr  6910  1idsr  6911  archsr  6924  prsradd  6928  prsrlt  6929  caucvgsr  6944  elrealeu  6964  muladd11r  7230  negeu  7265  pncan  7280  pncan3  7282  negsub  7322  addid0  7443  posdif  7524  ltnegcon1  7532  subge0  7544  suble0  7545  lesub0  7548  reapval  7641  reapneg  7662  ap0gt0  7703  recextlem1  7706  div0ap  7753  recrecap  7760  rec11ap  7761  recgt0  7891  mulgt1  7904  lerec2  7930  recp1lt1  7940  recreclt  7941  ledivp1  7944  nnsub  8028  avglt1  8220  nnrecl  8237  nnnn0addcl  8269  elnn0nn  8281  nn0ge2m1nn  8299  zaddcl  8342  eluzadd  8597  divfnzn  8653  qaddcl  8667  qreccl  8674  cnref1o  8680  ge0p1rp  8712  divlt1lt  8748  divle1le  8749  addlelt  8786  xrre3  8836  xltnegi  8849  ixxssixx  8872  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  zltaddlt1le  8975  elfz2  8983  peano2fzr  9003  fzdcel  9006  fzsplit2  9016  fzaddel  9024  fzrev2  9049  fzrev2i  9050  fzrev3  9051  elfz1b  9054  fseq1p1m1  9058  uzsubfz0  9088  fzosubel3  9154  eluzgtdifelfzo  9155  fzofzp1b  9186  elfzomelpfzo  9189  fvinim0ffz  9198  qbtwnxr  9214  ico0  9218  flqge  9232  flqlt  9233  flqltnz  9237  flqbi2  9241  flqaddz  9247  flqmulnn0  9249  intfracq  9270  flqdiv  9271  q0mod  9305  q1mod  9306  mulp1mod1  9315  q2txmodxeq0  9334  modfzo0difsn  9345  frec2uzuzd  9352  frec2uzltd  9353  frec2uzrand  9355  iseqsplit  9402  iseqcaopr  9406  expivallem  9421  expival  9422  expinnval  9423  exp1  9426  expcl2lemap  9432  rpexpcl  9439  expnegzap  9454  mulexp  9459  mulexpzap  9460  leexp2r  9474  leexp1a  9475  sq11  9492  subsq  9525  binom2  9529  binom3  9534  zesq  9535  bernneq  9537  sq11ap  9583  facwordi  9608  facubnd  9613  facavg  9614  bcval  9617  ibcval5  9631  shftfvalg  9647  ovshftex  9648  shftdm  9651  shftfib  9652  shftval  9654  shftf  9659  crre  9685  cjexp  9721  cjreim2  9732  uzin2  9814  rexuz3  9817  resqrexlemgt0  9847  resqrex  9853  sqrtgt0  9861  sqrtsq  9871  sqrtmsq  9872  absrpclap  9888  absext  9890  absmul  9896  absid  9898  absexp  9906  nn0abscl  9912  abslt  9915  absle  9916  recvalap  9924  abstri  9931  caubnd2  9944  qdenre  10029  climconst2  10043  climmpt  10052  climres  10055  climcaucn  10101  sumeq1  10105  dvdsdc  10116  iddvdsexp  10131  dvdsadd  10150  dvds1  10165  odd2np1  10184  oddm1even  10186  m1exp1  10213  divalglemnn  10230  fldivndvdslt  10247  flodddiv4lt  10248  pw2dvdslemn  10253  oddpwdclemdc  10261  bj-indind  10443  bj-omtrans  10468  bj-inf2vnlem1  10482  sscoll2  10500  qdencn  10511
  Copyright terms: Public domain W3C validator