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

Theorem simpl 102
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 99 1 ((𝜑𝜓) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-ia1 99
This theorem is referenced by:  simpli  104  simpld  105  imp  115  adantrd  264  iba  284  pm3.41  314  pm4.45im  317  prth  326  pm4.71  369  adantlr  446  adantrr  448  adantllr  450  adantlrr  452  adantrlr  454  adantrrr  456  simplll  485  simplrl  487  simprll  489  simprrl  491  anabs1  506  jcab  535  pm4.38  537  pm5.21  611  ioran  669  pm3.14  670  pm4.44  696  ordi  729  pm4.39  735  pm5.16  737  pm5.54dc  827  intnanr  839  intnanrd  841  dcan  842  dedlema  876  dedlemb  877  pm4.42r  878  prlem2  881  simp1l  928  simp2l  930  simp3l  932  3anandis  1237  xordc1  1284  anxordi  1291  falantru  1294  19.26  1370  exsimpl  1508  sbequ2  1652  sbcof2  1691  sbequilem  1719  sbequ8  1727  euan  1956  mooran1  1972  eupickbi  1982  2exeu  1992  dimatis  2017  rexim  2413  r19.26  2441  r19.40  2464  rr19.28v  2683  elrab3t  2697  eueq3dc  2715  mosubt  2718  reu6  2730  sbc2iegf  2828  sbcralt  2834  sbcrext  2835  rmob  2850  csbiebt  2886  ssab2  3024  difdif  3069  uneqin  3188  indifdir  3193  undif3ss  3198  rexm  3320  difsn  3501  opprc1  3571  unissel  3609  ssmin  3634  abssexg  3934  opelopabsb  3997  sess1  4074  ordelord  4118  onin  4123  suctr  4158  ordtriexmidlem  4245  ordtri2or2exmid  4296  tfi  4305  peano1  4317  peano2  4318  0nelxp  4372  0nelelxp  4373  brab2a  4393  mosubopt  4405  posng  4412  opabssxp  4414  ideqg  4487  relssres  4648  trin2  4716  dminss  4738  iota4an  4886  iota2  4893  fun11uni  4969  imadiflem  4978  funimaexg  4983  fneq12  4992  fvelrnb  5221  dffo4  5315  ffnfv  5323  ffvresb  5328  fmptco  5330  fcoconst  5334  fcof1  5423  isotr  5456  isopolem  5461  f1oiso  5465  acexmidlemcase  5507  ovprc1  5541  fnoprabg  5602  op1steq  5805  1stconst  5842  f1o2ndf1  5849  sprmpt2  5857  brtpos2  5866  tpostpos  5879  tposf12  5884  smores  5907  tfrlemi1  5946  freceq1  5979  freceq2  5980  frectfr  5985  omv2  6045  omsuc  6051  nnsucelsuc  6070  nntri3  6075  nnaordi  6081  nnmordi  6089  nnm00  6102  ecexr  6111  ertr  6121  swoer  6134  erth  6150  ecelqsdm  6176  iinerm  6178  ecinxp  6181  erovlem  6198  dom3  6256  phpelm  6328  nnwetri  6354  ordiso2  6357  dmaddpqlem  6475  distrnqg  6485  ltanqi  6500  ltmnqi  6501  ltaddnq  6505  ltrnqg  6518  ltnnnq  6521  enq0sym  6530  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  distrnq0  6557  prarloclemn  6597  prarloc  6601  ltdfpr  6604  genplt2i  6608  addnqprl  6627  addnqpru  6628  nqprl  6649  appdivnq  6661  1idprl  6688  1idpru  6689  ltexpri  6711  recexpr  6736  cauappcvgprlemdisj  6749  archrecpr  6762  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  0idsr  6852  1idsr  6853  archsr  6866  prsradd  6870  prsrlt  6871  caucvgsr  6886  elrealeu  6906  negeu  7202  pncan  7217  pncan3  7219  negsub  7259  posdif  7450  ltnegcon1  7458  subge0  7470  suble0  7471  lesub0  7474  reapval  7567  reapneg  7588  ap0gt0  7629  recextlem1  7632  div0ap  7679  recrecap  7685  rec11ap  7686  recgt0  7816  mulgt1  7829  lerec2  7855  recp1lt1  7865  recreclt  7866  ledivp1  7869  nnsub  7952  avglt1  8163  nnrecl  8179  nnnn0addcl  8212  elnn0nn  8224  nn0ge2m1nn  8242  zaddcl  8285  eluzadd  8501  divfnzn  8556  qaddcl  8570  qreccl  8576  cnref1o  8582  ge0p1rp  8614  divlt1lt  8650  divle1le  8651  xrre3  8735  xltnegi  8748  ixxssixx  8771  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  elfz2  8881  peano2fzr  8901  fzdcel  8904  fzsplit2  8914  fzaddel  8922  fzrev2  8947  fzrev2i  8948  fzrev3  8949  elfz1b  8952  fseq1p1m1  8956  uzsubfz0  8986  fzosubel3  9052  eluzgtdifelfzo  9053  fzofzp1b  9084  elfzomelpfzo  9087  fvinim0ffz  9096  flqge  9124  flqlt  9125  flqltnz  9129  flqbi2  9133  flqaddz  9139  flqmulnn0  9141  intfracq  9162  flqdiv  9163  frec2uzuzd  9188  frec2uzltd  9189  frec2uzrand  9191  iseqsplit  9238  iseqcaopr  9242  expivallem  9256  expival  9257  expinnval  9258  exp1  9261  expcl2lemap  9267  rpexpcl  9274  expnegzap  9289  mulexp  9294  mulexpzap  9295  leexp2r  9308  leexp1a  9309  sq11  9326  subsq  9358  binom2  9362  binom3  9366  zesq  9367  bernneq  9369  sq11ap  9414  shftfvalg  9419  ovshftex  9420  shftdm  9423  shftfib  9424  shftval  9426  shftf  9431  crre  9457  cjexp  9493  cjreim2  9504  uzin2  9586  rexuz3  9588  resqrexlemgt0  9618  resqrex  9624  sqrtgt0  9632  sqrtsq  9642  sqrtmsq  9643  absrpclap  9659  absext  9661  absmul  9667  absid  9669  absexp  9675  nn0abscl  9681  abslt  9684  absle  9685  recvalap  9693  abstri  9700  caubnd2  9713  qdenre  9798  climconst2  9812  climmpt  9821  climres  9824  climcaucn  9870  sumeq1  9874  bj-indind  10056  bj-omtrans  10081  bj-inf2vnlem1  10095  sscoll2  10113  qdencn  10124
  Copyright terms: Public domain W3C validator