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  6355  dmaddpqlem  6473  distrnqg  6483  ltanqi  6498  ltmnqi  6499  ltaddnq  6503  ltrnqg  6516  ltnnnq  6519  enq0sym  6528  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  distrnq0  6555  prarloclemn  6595  prarloc  6599  ltdfpr  6602  genplt2i  6606  addnqprl  6625  addnqpru  6626  nqprl  6647  appdivnq  6659  1idprl  6686  1idpru  6687  ltexpri  6709  recexpr  6734  cauappcvgprlemdisj  6747  archrecpr  6760  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  0idsr  6850  1idsr  6851  archsr  6864  prsradd  6868  prsrlt  6869  caucvgsr  6884  elrealeu  6904  negeu  7200  pncan  7215  pncan3  7217  negsub  7257  posdif  7448  ltnegcon1  7456  subge0  7468  suble0  7469  lesub0  7472  reapval  7565  reapneg  7586  ap0gt0  7627  recextlem1  7630  div0ap  7677  recrecap  7683  rec11ap  7684  recgt0  7814  mulgt1  7827  lerec2  7853  recp1lt1  7863  recreclt  7864  ledivp1  7867  nnsub  7950  avglt1  8161  nnrecl  8177  nnnn0addcl  8210  elnn0nn  8222  nn0ge2m1nn  8240  zaddcl  8283  eluzadd  8499  divfnzn  8554  qaddcl  8568  qreccl  8574  cnref1o  8580  ge0p1rp  8612  divlt1lt  8648  divle1le  8649  xrre3  8733  xltnegi  8746  ixxssixx  8769  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  elfz2  8879  peano2fzr  8899  fzdcel  8902  fzsplit2  8912  fzaddel  8920  fzrev2  8945  fzrev2i  8946  fzrev3  8947  elfz1b  8950  fseq1p1m1  8954  uzsubfz0  8984  fzosubel3  9050  eluzgtdifelfzo  9051  fzofzp1b  9082  elfzomelpfzo  9085  fvinim0ffz  9094  flqge  9122  flqlt  9123  flqltnz  9127  flqbi2  9131  flqaddz  9137  flqmulnn0  9139  frec2uzuzd  9162  frec2uzltd  9163  frec2uzrand  9165  iseqsplit  9212  iseqcaopr  9216  expivallem  9230  expival  9231  expinnval  9232  exp1  9235  expcl2lemap  9241  rpexpcl  9248  expnegzap  9263  mulexp  9268  mulexpzap  9269  leexp2r  9282  leexp1a  9283  sq11  9300  subsq  9332  binom2  9336  binom3  9340  zesq  9341  bernneq  9343  sq11ap  9388  shftfvalg  9393  ovshftex  9394  shftdm  9397  shftfib  9398  shftval  9400  shftf  9405  crre  9431  cjexp  9467  cjreim2  9478  uzin2  9560  rexuz3  9562  resqrexlemgt0  9592  resqrex  9598  sqrtgt0  9606  sqrtsq  9616  sqrtmsq  9617  absrpclap  9633  absext  9635  absmul  9641  absid  9643  absexp  9649  nn0abscl  9655  abslt  9658  absle  9659  recvalap  9667  abstri  9674  caubnd2  9687  qdenre  9772  climconst2  9786  climmpt  9795  climres  9798  climcaucn  9844  sumeq1  9848  bj-indind  10030  bj-omtrans  10055  bj-inf2vnlem1  10069  sscoll2  10087
  Copyright terms: Public domain W3C validator