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

Theorem simpl 107
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 104 1 ((𝜑𝜓) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-ia1 104
This theorem is referenced by:  simpli  109  simpld  110  imp  122  adantrd  273  iba  294  pm3.41  324  pm4.45im  327  prth  336  pm4.71  381  adantlr  461  adantrr  463  adantllr  465  adantlrr  467  adantrlr  469  adantrrr  471  simplll  500  simplrl  502  simprll  504  simprrl  506  anabs1  537  jcab  568  pm4.38  570  pm5.21  644  ioran  702  pm3.14  703  pm4.44  729  ordi  763  pm4.39  769  pm5.16  771  pm5.54dc  863  intnanr  875  intnanrd  877  dcan  878  dedlema  913  dedlemb  914  pm4.42r  915  prlem2  918  simp1l  965  simp2l  967  simp3l  969  3anandis  1281  xordc1  1327  anxordi  1334  falantru  1337  19.26  1413  exsimpl  1551  sbequ2  1696  sbcof2  1735  sbequilem  1763  sbequ8  1772  euan  2001  mooran1  2017  eupickbi  2027  2exeu  2037  dimatis  2062  rexim  2463  r19.26  2493  r19.40  2517  rr19.28v  2747  elrab3t  2761  eueq3dc  2780  mosubt  2783  reu6  2795  sbc2iegf  2898  sbcralt  2904  sbcrext  2905  rmob  2920  csbiebt  2956  ssab2  3094  difdif  3114  uneqin  3239  indifdir  3244  undif3ss  3249  rexm  3368  eqifdc  3411  ifandc  3413  difsn  3557  opprc1  3627  unissel  3665  ssmin  3690  abssexg  3991  undifexmid  4002  exmidundif  4009  opelopabsb  4061  sess1  4138  ordelord  4182  onin  4187  suctr  4222  ordtriexmidlem  4309  ordtri2or2exmid  4360  tfi  4370  peano1  4382  peano2  4383  0nelxp  4438  0nelelxp  4439  brab2a  4459  mosubopt  4471  posng  4478  opabssxp  4480  ideqg  4555  relssres  4717  trin2  4790  dminss  4812  iota4an  4965  iota2  4972  fun11uni  5049  imadiflem  5058  funimaexg  5063  fneq12  5072  fvelrnb  5315  dffo4  5410  ffnfv  5419  ffvresb  5424  fmptco  5427  fcoconst  5431  fcof1  5523  isotr  5556  isopolem  5562  f1oiso  5566  acexmidlemcase  5608  ovprc1  5642  fnoprabg  5703  op1steq  5906  1stconst  5943  f1o2ndf1  5950  sprmpt2  5961  brtpos2  5970  tpostpos  5983  tposf12  5988  smores  6011  tfrlemi1  6051  tfr1onlembfn  6063  tfri1dALT  6070  tfrcllembfn  6076  freceq1  6111  freceq2  6112  frectfr  6119  omv2  6180  omsuc  6187  nnsucelsuc  6206  nntri3  6212  nnaordi  6219  nnmordi  6227  nnm00  6240  ecexr  6249  ertr  6259  swoer  6272  erth  6288  ecelqsdm  6314  iinerm  6316  ecinxp  6319  erovlem  6336  pmresg  6385  dom3  6445  mapdom1g  6515  ssenen  6519  phpelm  6534  finexdc  6570  nnwetri  6578  supubti  6638  supisoex  6648  ordiso2  6672  djuun  6704  nnnninf  6750  en2eleq  6765  en2other2  6766  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  dmaddpqlem  6880  distrnqg  6890  ltanqi  6905  ltmnqi  6906  ltaddnq  6910  ltrnqg  6923  ltnnnq  6926  enq0sym  6935  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  distrnq0  6962  prarloclemn  7002  prarloc  7006  ltdfpr  7009  genplt2i  7013  addnqprl  7032  addnqpru  7033  nqprl  7054  appdivnq  7066  1idprl  7093  1idpru  7094  ltexpri  7116  recexpr  7141  cauappcvgprlemdisj  7154  archrecpr  7167  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  0idsr  7257  1idsr  7258  archsr  7271  prsradd  7275  prsrlt  7276  caucvgsr  7291  elrealeu  7311  muladd11r  7582  negeu  7617  pncan  7632  pncan3  7634  negsub  7674  addid0  7795  posdif  7877  ltnegcon1  7885  subge0  7897  suble0  7898  lesub0  7901  reapval  7994  reapneg  8015  ap0gt0  8056  recextlem1  8059  div0ap  8108  recrecap  8115  rec11ap  8116  recgt0  8246  mulgt1  8259  lerec2  8285  recp1lt1  8295  recreclt  8296  ledivp1  8299  negiso  8351  nnsub  8395  avglt1  8587  nnrecl  8604  nnnn0addcl  8636  elnn0nn  8648  nn0ge2m1nn  8666  zaddcl  8723  eluzadd  8979  divfnzn  9038  qaddcl  9052  qreccl  9059  cnref1o  9065  ge0p1rp  9097  divlt1lt  9133  divle1le  9134  addlelt  9171  xrre3  9216  xltnegi  9229  ixxssixx  9252  iccshftr  9343  iccshftl  9345  iccdil  9347  icccntr  9349  zltaddlt1le  9355  elfz2  9363  peano2fzr  9383  fzdcel  9386  fzsplit2  9396  fzaddel  9404  fzrev2  9429  fzrev2i  9430  fzrev3  9431  elfz1b  9434  fseq1p1m1  9438  uzsubfz0  9468  fzosubel3  9535  eluzgtdifelfzo  9536  fzofzp1b  9567  elfzomelpfzo  9570  exfzdc  9579  fvinim0ffz  9580  exbtwnzlemshrink  9588  qbtwnz  9591  qbtwnxr  9597  ico0  9601  apbtwnz  9609  flqge  9617  flqlt  9618  flqltnz  9622  flqbi2  9626  flqaddz  9632  flqmulnn0  9634  intfracq  9655  flqdiv  9656  q0mod  9690  q1mod  9691  mulp1mod1  9700  q2txmodxeq0  9719  modfzo0difsn  9730  frec2uzuzd  9737  frec2uzltd  9738  frec2uzrand  9740  iseqsplit  9812  iseqcaopr  9816  expivallem  9854  expival  9855  expinnval  9856  exp1  9859  expcl2lemap  9865  rpexpcl  9872  expnegzap  9887  mulexp  9892  mulexpzap  9893  leexp2r  9907  leexp1a  9908  sq11  9925  subsq  9958  binom2  9962  binom3  9967  zesq  9968  bernneq  9970  sq11ap  10016  facwordi  10044  facubnd  10049  facavg  10050  bcval  10053  ibcval5  10067  hashennn  10084  fihashf1rn  10093  fseq1hash  10105  hashdifsn  10123  hashdifpr  10124  hashxp  10130  fnfz0hash  10133  ffzo0hash  10135  shftfvalg  10148  ovshftex  10149  shftdm  10152  shftfib  10153  shftval  10155  shftf  10160  crre  10186  cjexp  10222  cjreim2  10233  uzin2  10315  rexuz3  10318  resqrexlemgt0  10348  resqrex  10354  sqrtgt0  10362  sqrtsq  10372  sqrtmsq  10373  absrpclap  10389  absext  10391  absmul  10397  absid  10399  absexp  10407  nn0abscl  10413  abslt  10416  absle  10417  recvalap  10425  abstri  10432  caubnd2  10445  qdenre  10530  maxabsle  10532  maxabslemval  10536  maxcl  10538  rexanre  10548  min1inf  10555  climconst2  10572  climmpt  10581  climres  10584  climcaucn  10630  sumeq1  10634  isummolem2a  10660  isumz  10667  fisumss  10670  dvdsdc  10679  iddvdsexp  10695  dvdsadd  10714  dvds1  10729  odd2np1  10748  oddm1even  10750  m1exp1  10776  divalglemnn  10793  fldivndvdslt  10810  flodddiv4lt  10811  zsupcllemex  10817  infssuzcldc  10822  dvdsbnd  10823  gcdnncl  10834  zeqzmulgcd  10837  gcdneg  10848  modgcd  10857  bezoutlemex  10865  bezoutlemeu  10871  dfgcd3  10874  gcdzeq  10886  dvdssq  10895  eucalgval2  10910  eucialgcvga  10915  lcmval  10920  gcddvdslcm  10930  lcmneg  10931  coprmgcdb  10945  qredeu  10954  divgcdcoprm0  10958  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  cncongrcoprm  10963  prmind2  10977  dvdsnprmd  10982  exprmfct  10994  isprm6  11001  pw2dvdslemn  11018  oddpwdclemdc  11026  sqrt2irraplemnn  11032  divnumden  11049  divdenle  11050  nn0sqrtelqelz  11059  phivalfi  11063  crth  11075  xpct  11084  znnen  11086  bj-indind  11265  bj-omtrans  11289  bj-inf2vnlem1  11303  sscoll2  11321  nnpredcl  11328  nninfsellemsuc  11342  nninfomnilem  11348  exmidsbthrlem  11350  qdencn  11353
  Copyright terms: Public domain W3C validator