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

Theorem simpr 108
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  |-  ( (
ph  /\  ps )  ->  ps )

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 105 1  |-  ( (
ph  /\  ps )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-ia2 105
This theorem is referenced by:  simpri  111  simprd  112  imp  122  adantld  272  ibar  295  pm3.42  325  pm3.4  326  prth  336  simpl2im  378  sylancom  411  adantll  460  adantrl  462  adantlll  464  adantlrl  466  adantrll  468  adantrrl  470  simpllr  501  simplrr  503  simprlr  505  simprrr  507  anabs7  539  jcab  568  pm4.38  570  pm5.21  644  ioran  702  pm3.14  703  ordi  763  pm4.39  769  pm5.16  771  pm5.54dc  863  intnan  874  intnand  876  dcan  878  bimsc1  907  niabn  911  simp1r  966  simp2r  968  simp3r  970  3anandirs  1282  bilukdc  1330  19.26  1413  exsimpr  1552  19.40  1565  cbvexh  1682  sbequilem  1763  spsbe  1767  cbvexdh  1846  euan  2001  moan  2014  datisi  2055  fresison  2063  rexex  2418  r19.26  2493  r19.29an  2506  r19.40  2517  cbvraldva2  2590  cbvrexdva2  2591  gencbvex  2659  rspct  2708  rspcimdv  2716  rspcimedv  2717  rr19.28v  2747  elrab3t  2761  reu6  2795  rmob  2920  csbiebt  2956  rabssab  3097  ssddif  3222  difin  3225  difrab  3262  eqifdc  3411  ifmdc  3414  preqsn  3602  opprc2  3628  dfnfc2  3654  intmin4  3699  sndisj  3816  undifexmid  4002  exmid01  4006  exmidundif  4009  exss  4028  euotd  4055  frirrg  4151  suctr  4222  ordtri2or2exmid  4360  wetriext  4365  reg3exmidlemwe  4367  tfisi  4375  peano2  4383  omsinds  4408  relop  4554  releldm  4638  relelrn  4639  resiexg  4724  trin2  4790  xpmlem  4818  unielrel  4924  relcoi2  4927  iota2df  4970  iota2  4972  funopab4  5016  fun11uni  5049  imadiflem  5058  imain  5061  fneq12  5072  f1ssr  5186  fvelrnb  5315  ssimaex  5328  fvmpt2d  5352  fvmptdf  5353  dffo3  5409  ffvresb  5424  fmptco  5427  funfvima3  5489  f1imass  5514  fliftf  5539  fliftval  5540  riota2df  5589  riota5f  5593  acexmidlemcase  5608  ovprc2  5643  eloprabga  5692  eqfnov2  5709  ovmpt2dxf  5727  fnofval  5822  offval2  5827  ofrfval2  5828  caofinvl  5834  2ndrn  5910  1st2ndbr  5911  cnvf1o  5947  f1o2ndf1  5950  mpt2xopoveq  5959  sprmpt2  5961  dftpos4  5982  tpostpos  5983  tposf12  5988  dfsmo2  6006  smores  6011  tfrlem1  6027  tfrlem3ag  6028  tfrlem3a  6029  tfrlemisucaccv  6044  tfrlemi1  6051  tfrexlem  6053  tfr1onlem3ag  6056  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemaccex  6067  tfr1onlemres  6068  tfri1dALT  6070  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemaccex  6080  tfrcllemres  6081  tfrcl  6083  rdgivallem  6100  rdgon  6105  frecabex  6117  frecabcl  6118  frectfr  6119  frecrdg  6127  oawordi  6184  nntri3  6212  dcdifsnid  6217  nnaordi  6219  nnaordex  6238  nnawordex  6239  nnm00  6240  ersymb  6258  ertr  6259  erref  6264  iserd  6270  swoer  6272  erth  6288  iinerm  6316  erinxp  6318  ecinxp  6319  qsel  6321  qliftel  6324  qliftfun  6326  fvdiagfn  6402  dom3  6445  ssdomg  6447  cnven  6477  xpen  6513  xpmapenlem  6517  ssenen  6519  phplem4dom  6530  phpm  6533  phpelm  6534  fidifsnen  6538  fin0  6553  fin0or  6554  isinfinf  6565  tridc  6567  fimax2gtrilemstep  6568  fimax2gtri  6569  finexdc  6570  en2eqpr  6575  fientri3  6577  unsnfidcex  6582  unsnfidcel  6583  unfidisj  6584  undifdcss  6585  undifdc  6586  unfiin  6588  fnfi  6596  relcnvfi  6600  f1dmvrnfibi  6603  f1finf1o  6605  suplubti  6639  suplub2ti  6640  supelti  6641  supisolem  6647  supisoex  6648  infglbti  6664  ordiso2  6672  djuss  6705  updjudhcoinlf  6715  updjudhcoinrg  6716  updjud  6717  djudom  6731  enomnilem  6738  finomni  6740  exmidomni  6742  fodjuomnilemdc  6743  fodjuomnilemres  6747  nnnninf  6750  en2eleq  6765  en2other2  6766  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  dmaddpqlem  6880  nqpi  6881  mulcanenq  6888  ltaddnq  6910  ltexnqq  6911  prarloclemarch2  6922  ltrnqg  6923  ltnnnq  6926  enq0sym  6935  nqnq0pi  6941  nq0nn  6945  mulcanenq0ec  6948  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  prloc  6994  prarloclemlt  6996  prarloclemlo  6997  ltdfpr  7009  genplt2i  7013  genpml  7020  genpmu  7021  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  nqprloc  7048  appdivnq  7066  appdiv0nq  7067  mulnqprl  7071  mulnqpru  7072  distrlem1prl  7085  distrlem1pru  7086  ltprordil  7092  1idprl  7093  1idpru  7094  ltexprlemrl  7113  ltexprlemru  7115  ltexpri  7116  addcanprleml  7117  addcanprlemu  7118  recexprlem1ssl  7136  recexpr  7141  aptiprlemu  7143  archpr  7146  cauappcvgprlemopl  7149  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemval  7191  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlemlim  7214  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  0idsr  7257  1idsr  7258  recexsrlem  7264  addgt0sr  7265  srpospr  7272  prsradd  7275  prsrlt  7276  caucvgsrlemfv  7280  caucvgsrlemgt1  7284  caucvgsrlemoffval  7285  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  rereceu  7368  axarch  7370  nntopi  7373  axcaucvglemval  7376  muladd11r  7582  cnegexlem1  7601  cnegex  7604  negeu  7617  pncan  7632  pncan3  7634  npcan  7635  addid0  7795  negf1o  7804  mulneg1  7817  lelttrdi  7848  ltnegcon2  7886  add20  7896  subge0  7897  lesub0  7901  reapval  7994  recexre  7996  apreap  8005  ltmul1a  8009  reapneg  8015  cru  8020  apsym  8024  apcotr  8025  apadd1  8026  apneg  8029  mulext1  8030  apti  8040  gt0ap0  8043  ap0gt0  8056  recexap  8061  divmulassap  8101  divmulasscomap  8102  rerecclap  8136  recgt0  8246  prodgt0gt0  8247  lemul1a  8254  lemul12a  8258  lt2msq  8282  ltrec1  8284  recreclt  8296  negiso  8351  creui  8355  cju  8356  avglt2  8588  un0addcl  8639  nn0ge2m1nn  8666  nn0nndivcl  8668  elnn0z  8696  peano2z  8719  elz2  8751  suprzclex  8777  peano5uzti  8787  zindd  8797  eluzadd  8979  nn0pzuz  9007  supinfneg  9015  infsupneg  9016  eluz2b2  9022  eqreznegel  9031  nn0ge2m1nnALT  9035  divfnzn  9038  qmulz  9040  qapne  9056  qreccl  9059  cnref1o  9065  ge0p1rp  9097  xrltso  9198  z2ge  9220  xltnegi  9229  ixxssixx  9252  lincmb01cmp  9352  iccf1o  9353  zltaddlt1le  9355  fztri3or  9385  fzdcel  9386  fznlem  9387  fzn  9388  uzsubsubfz  9393  fzsplit2  9396  fzopth  9406  fzdifsuc  9425  fzrev2i  9430  elfz1b  9434  fzneuz  9445  fzrevral  9449  ige2m1fz  9454  elfz0ubfz0  9464  elfz0fzfz0  9465  4fvwrd4  9479  2ffzeq  9480  fzospliti  9515  fzosplit  9516  fzo1fzo0n0  9522  fzonmapblen  9526  fzoaddel  9531  fzosubel  9533  fzosubel3  9535  elfzodifsumelfzo  9540  elfzom1elp1fzo  9541  elfzom1p1elfzo  9553  elfzonelfzo  9569  peano2fzor  9571  exfzdc  9579  fvinim0ffz  9580  qtri3or  9582  exbtwnzlemstep  9587  rebtwn2zlemstep  9592  qbtwnxr  9597  apbtwnz  9609  flqge  9617  flqltnz  9622  flqaddz  9632  btwnzge0  9635  flltdivnn0lt  9639  intfracq  9655  flqdiv  9656  modqid0  9685  q0mod  9690  q1mod  9691  modqmuladdim  9702  modqmuladdnn0  9703  q2txmodxeq0  9719  q2submod  9720  modifeq2int  9721  modqsubdir  9728  modsumfzodifsn  9731  addmodlteq  9733  frec2uzzd  9735  frec2uzuzd  9737  frec2uzrand  9740  frec2uzf1od  9741  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgg  9751  frecuzrdgdomlem  9752  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  frecfzennn  9761  uzsinds  9776  iseqvalt  9790  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfeq2  9803  iseqfeq  9805  isermono  9811  iseqsplit  9812  iseqf1olemkle  9817  iseqf1olemklt  9818  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemab  9822  iseqf1olemqf  9824  iseqf1olemmo  9825  iseqf1olemqf1o  9826  iseqf1olemqk  9827  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1oleml  9836  iseqf1o  9837  iseqid3s  9841  iseqid  9842  iseqhomo  9844  iseqz  9845  fser0const  9849  expivallem  9854  expival  9855  expinnval  9856  expp1  9860  rpexpcl  9872  expaddzaplem  9896  leexp1a  9908  exple1  9909  subsq  9958  binom2  9962  binom3  9967  bernneq3  9972  expnbnd  9973  expcan  10021  nn0opthd  10026  faclbnd  10045  faclbnd6  10048  facubnd  10049  facavg  10050  bcval  10053  bccmpl  10058  ibcval5  10067  bcpasc  10070  hashennnuni  10083  hashennn  10084  hashfiv01gt1  10086  fihasheqf1oi  10092  hashnncl  10100  fseq1hash  10105  fiprsshashgt1  10121  fimaxq  10131  fnfz0hash  10133  ffzo0hash  10135  zfz1isolemiso  10140  zfz1iso  10142  iseqcoll  10143  shftfvalg  10148  ovshftex  10149  shftdm  10152  shftfib  10153  shftval  10155  shftval5  10159  shftf  10160  2shfti  10161  crre  10186  rereb  10192  cjreim2  10233  cjap  10235  caucvgrelemrec  10307  caucvgrelemcau  10308  caucvgre  10309  cvg1nlemf  10311  cvg1nlemres  10313  uzin2  10315  rexuz3  10318  recvguniq  10323  sqrt0  10332  resqrexlemdecn  10340  resqrexlemlo  10341  resqrexlemcalc3  10344  resqrexlemnm  10346  resqrexlemcvg  10347  resqrexlemoverl  10349  resqrexlemglsq  10350  resqrexlemga  10351  resqrex  10354  sqrtgt0  10362  absrpclap  10389  absext  10391  absmul  10397  leabs  10402  nn0abscl  10413  ltabs  10415  abslt  10416  absle  10417  abssubap0  10418  abstri  10432  cau3lem  10442  caubnd2  10445  maxabsle  10532  maxabslemlub  10535  maxabslemval  10536  maxcl  10538  maxleastb  10542  maxltsup  10546  rexanre  10548  rexico  10549  fimaxre2  10551  minmax  10554  min2inf  10556  clim  10562  climi2  10569  climconst2  10572  climuni  10574  climmpt  10581  climshftlemg  10583  climres  10584  climcn1  10589  subcn2  10592  cn1lem  10594  climadd  10606  climmul  10607  climsub  10608  climle  10614  climsqz  10615  climsqz2  10616  clim2iser  10617  clim2iser2  10618  iiserex  10619  iisermulc2  10620  iserile  10622  iserige0  10623  climub  10624  climserile  10625  climrecvg1n  10627  climcvg1nlem  10628  serif0  10631  sumeq2  10638  sumfct  10653  isumrblem  10655  fisumcvg  10656  isumrb  10657  isummolem2a  10660  isummolem2  10661  isummo  10662  zisum  10663  iisum  10664  fisum  10665  sum0  10666  isumz  10667  fsumf1o  10668  isumss  10669  fisumss  10670  dvdsval2  10674  dvdsdc  10679  moddvds  10680  zdvdsdc  10692  dvdscmul  10698  dvdsmulc  10699  dvdscmulr  10700  dvdsmulcr  10701  modmulconst  10703  dvdsadd  10714  dvdsadd2b  10718  dvdslelemd  10719  dvdsle  10720  dvdsabseq  10723  dvdseq  10724  divconjdvds  10725  dvds1  10729  fzo0dvdseq  10733  dvdsmod  10738  oddm1even  10750  mod2eq1n2dvds  10754  evennn02n  10757  evennn2n  10758  divalglemnn  10793  divalglemnqt  10795  divalglemeunn  10796  divalglemex  10797  divalglemeuneg  10798  divalg  10799  divalgmod  10802  modremain  10804  infssuzex  10820  gcdsupex  10824  gcdsupcl  10825  gcdval  10826  dvdslegcd  10831  gcdnncl  10834  gcdneg  10848  gcdaddm  10850  gcd1  10853  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemzz  10866  bezoutlemaz  10867  bezoutlembz  10868  bezoutlembi  10869  bezoutlemle  10872  bezoutlemsup  10873  gcdass  10879  gcdzeq  10886  dvdsmulgcd  10889  bezoutr1  10897  ialgrp1  10903  ialgcvga  10908  eucalgval2  10910  eucalgf  10912  eucalglt  10914  lcmval  10920  lcmledvds  10927  lcmneg  10931  lcmgcd  10935  lcmid  10937  coprmgcdb  10945  ncoprmgcdne1b  10946  mulgcddvds  10951  rpmulgcd2  10952  qredeq  10953  divgcdcoprm0  10958  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  isprm2lem  10973  prmind2  10977  sqnprm  10992  isprm6  11001  prmdvdsexp  11002  prmfac1  11006  rpexp  11007  rpexp1i  11008  sqrt2irr  11016  pw2dvdslemn  11018  pw2dvdseulemle  11020  oddpwdclemxy  11022  oddpwdclemdc  11026  oddpwdc  11027  znege1  11031  sqrt2irraplemnn  11032  sqrt2irrap  11033  divnumden  11049  qden1elz  11058  phibndlem  11067  dfphi2  11071  phiprmpw  11073  crth  11075  phimullem  11076  oddennn  11080  evenennn  11081  bj-indind  11265  bj-omtrans  11289  nnpredcl  11328  nnsf  11333  peano4nninf  11334  nninfalllemn  11336  nninfalllem1  11337  nninfall  11338  nninfself  11343  nninfsellemeq  11344  nninfsellemqall  11345  nninfsellemeqinf  11346  nninfsel  11347  nninfomnilem  11348  qdencn  11353
  Copyright terms: Public domain W3C validator