Theorem ad2antlr 489

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antlr	|- ( ( ( ch /\ ph ) /\ th ) -> ps )

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 476	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad3antlr  493  simplr  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4624  en2lp  4652  foun  5602  f1oprg  5629  fcof1o  5929  foeqcnvco  5930  f1eqcocnv  5931  caovord3  6195  f1o2ndf1  6392  smores2  6459  frecrdg  6573  nnaordex  6695  xpdom2  7014  xpen  7030  mapen  7031  xpmapenlem  7034  nndomo  7049  phpm  7051  fidifsnen  7056  isinfinf  7085  fidcen  7087  finexdc  7091  elssdc  7093  fientri3  7106  fiintim  7122  xpfi  7123  f1dmvrnfibi  7142  sbthlemi8  7162  djudom  7291  omp1eomlem  7292  difinfsn  7298  ctmlemr  7306  ctssdccl  7309  nnnninfeq  7326  enomnilem  7336  finomni  7338  ismkvnex  7353  enmkvlem  7359  nninfwlpoimlemginf  7374  exmidfodomrlemrALT  7413  exmidontriim  7439  netap  7472  exmidapne  7478  acnccim  7490  dfplpq2  7573  recclnq  7611  subhalfnqq  7633  distrnq0  7678  prarloclem3step  7715  genpml  7736  genpmu  7737  addnqprl  7748  addnqpru  7749  appdivnq  7782  mulnqprl  7787  mulnqpru  7788  mullocpr  7790  ltexprlemfl  7828  ltexprlemfu  7830  ltmprr  7861  archpr  7862  cauappcvgprlemm  7864  caucvgprlemladdrl  7897  caucvgprprlemopl  7916  caucvgprprlemopu  7918  recexgt0sr  7992  mulgt0sr  7997  elrealeu  8048  axcaucvglemcau  8117  axcaucvglemres  8118  cnegex  8356  apirr  8784  mulge0  8798  lemul12a  9041  lediv2a  9074  creur  9138  nndiv  9183  zaddcllemneg  9517  peano5uzti  9587  supinfneg  9828  infsupneg  9829  divfnzn  9854  xrltso  10030  xpncan  10105  xltadd1  10110  xleaddadd  10121  elioc2  10170  elico2  10171  elicc2  10172  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  exbtwnzlemex  10508  rebtwn2z  10513  modqid  10610  modqcyc  10620  mulqaddmodid  10625  modqadd2mod  10635  addmodlteq  10659  frecuzrdgg  10677  nninfinf  10704  seq3val  10721  seqvalcd  10722  seq3clss  10732  iseqf1olemqcl  10760  iseqf1olemnab  10762  seq3f1olemp  10776  seq3f1o  10778  seqf1oglem1  10780  seqfeq4g  10792  fser0const  10796  ser3ge0  10797  exp3vallem  10801  qsqeqor  10911  facndiv  11000  faclbnd  11002  bcval5  11024  hashen  11045  fihashdom  11065  hashunlem  11066  hashfacen  11099  zfz1isolemiso  11102  seq3coll  11105  ccatsymb  11178  ccatrn  11185  ccatw2s1p2  11222  swrdccatin1  11305  swrdccatin2  11309  swrdccat3b  11320  caucvgre  11541  resqrexlemlo  11573  cau3lem  11674  qdenre  11762  rexico  11781  fimaxre2  11787  2zinfmin  11803  xrmaxiflemcl  11805  xrmaxifle  11806  xrmaxiflemcom  11809  2clim  11861  cn1lem  11874  climsqz  11895  climsqz2  11896  climcau  11907  sumrbdclem  11937  summodclem2a  11941  fsum3  11947  fsumcl2lem  11958  fsumadd  11966  sumsnf  11969  fsum2dlemstep  11994  fisum0diag2  12007  fsummulc2  12008  mertenslemub  12094  mertenslemi1  12095  mertensabs  12097  ntrivcvgap  12108  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  prodmodc  12138  prod1dc  12146  prodsnf  12152  fprod2dlemstep  12182  efaddlem  12234  tanaddaplem  12298  zdvdsdc  12372  dvdseq  12408  dvdsext  12415  odd2np1  12433  sqoddm1div8z  12446  nno  12466  dfgcd3  12580  nninfctlemfo  12610  dvdslcm  12640  lcmneg  12645  lcmgcdlem  12648  ncoprmgcdne1b  12660  qredeq  12667  qredeu  12668  divgcdcoprm0  12672  exprmfct  12709  prmdvdsfz  12710  isprm5  12713  rpexp1i  12725  sqrt2irr  12733  nonsq  12778  eulerthlemrprm  12800  eulerthlema  12801  phisum  12812  modprmn0modprm0  12828  pclemdc  12860  pcz  12904  pcmpt  12915  fldivp1  12920  pcfac  12922  expnprm  12925  oddprmdvds  12926  prmpwdvds  12927  infpnlem1  12931  1arith  12939  4sqlem2  12961  4sqlemafi  12967  4sqleminfi  12969  4sqexercise2  12971  4sqlemsdc  12972  ctinfom  13048  enctlem  13052  nninfdclemlt  13071  setsfun  13116  setsfun0  13117  setscom  13121  gsumfzval  13473  mndissubm  13557  resmhm  13569  resmhm2  13570  mhmco  13572  gsumfzz  13577  gsumwsubmcl  13578  gsumwmhm  13580  dfgrp2  13609  isgrpinv  13636  mulgval  13708  mulgnnp1  13716  mulgz  13736  grpissubg  13780  resghm  13846  qusecsub  13917  isrng  13946  lmodfopne  14339  dflidl2rng  14494  gsumfzfsumlemm  14600  mulgrhm2  14623  znidomb  14671  znunit  14672  psrbaglesuppg  14685  psrbagfi  14686  tgdom  14795  ssrest  14905  cnfval  14917  cnpfval  14918  cnpval  14921  iscnp3  14926  ssidcn  14933  cnpnei  14942  cnntr  14948  cncnp  14953  cnptopresti  14961  tx1cn  14992  upxp  14995  imasnopn  15022  bdmet  15225  metcnp  15235  ivthinclemlr  15360  ivthinclemur  15362  ivthinc  15366  dvrecap  15436  dvmptfsum  15448  elply2  15458  plymullem1  15471  plycolemc  15481  plycjlemc  15483  dvply1  15488  pilem3  15506  relogeftb  15588  logbgcd1irr  15690  mpodvdsmulf1o  15713  mersenne  15720  lgslem4  15731  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsmod  15754  lgsdir2lem4  15759  lgsdinn0  15776  lgsquad2lem2  15810  lgsquad3  15812  2lgslem1c  15818  2sqlem6  15848  2sqlem7  15849  isupgren  15945  wrdupgren  15946  isumgren  15955  wrdumgren  15956  isuspgren  16007  isusgren  16008  clwwlkext2edg  16272  clwwlknonex2  16289  2omap  16594  pw1map  16596  nnsf  16607  peano4nninf  16608  nninfalllem1  16610  nninfsellemqall  16617  nninfsellemeqinf  16618  nninffeq  16622  exmidsbthrlem  16626  isomninnlem  16634  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656