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  4630  en2lp  4658  foun  5611  f1oprg  5638  fcof1o  5940  foeqcnvco  5941  f1eqcocnv  5942  caovord3  6206  f1o2ndf1  6402  suppfnss  6435  suppssdc  6438  suppssfvg  6441  smores2  6503  frecrdg  6617  nnaordex  6739  xpdom2  7058  xpen  7074  mapen  7075  xpmapenlem  7078  nndomo  7093  phpm  7095  fidifsnen  7100  isinfinf  7129  fidcen  7131  finexdc  7135  elssdc  7137  fientri3  7150  fiintim  7166  xpfi  7167  f1dmvrnfibi  7186  sbthlemi8  7206  djudom  7335  omp1eomlem  7336  difinfsn  7342  ctmlemr  7350  ctssdccl  7353  nnnninfeq  7370  enomnilem  7380  finomni  7382  ismkvnex  7397  enmkvlem  7403  nninfwlpoimlemginf  7418  exmidfodomrlemrALT  7457  exmidontriim  7483  netap  7516  exmidapne  7522  acnccim  7534  dfplpq2  7617  recclnq  7655  subhalfnqq  7677  distrnq0  7722  prarloclem3step  7759  genpml  7780  genpmu  7781  addnqprl  7792  addnqpru  7793  appdivnq  7826  mulnqprl  7831  mulnqpru  7832  mullocpr  7834  ltexprlemfl  7872  ltexprlemfu  7874  ltmprr  7905  archpr  7906  cauappcvgprlemm  7908  caucvgprlemladdrl  7941  caucvgprprlemopl  7960  caucvgprprlemopu  7962  recexgt0sr  8036  mulgt0sr  8041  elrealeu  8092  axcaucvglemcau  8161  axcaucvglemres  8162  cnegex  8399  apirr  8827  mulge0  8841  lemul12a  9084  lediv2a  9117  creur  9181  nndiv  9226  zaddcllemneg  9562  peano5uzti  9632  supinfneg  9873  infsupneg  9874  divfnzn  9899  xrltso  10075  xpncan  10150  xltadd1  10155  xleaddadd  10166  elioc2  10215  elico2  10216  elicc2  10217  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  exbtwnzlemex  10555  rebtwn2z  10560  modqid  10657  modqcyc  10667  mulqaddmodid  10672  modqadd2mod  10682  addmodlteq  10706  frecuzrdgg  10724  nninfinf  10751  seq3val  10768  seqvalcd  10769  seq3clss  10779  iseqf1olemqcl  10807  iseqf1olemnab  10809  seq3f1olemp  10823  seq3f1o  10825  seqf1oglem1  10827  seqfeq4g  10839  fser0const  10843  ser3ge0  10844  exp3vallem  10848  qsqeqor  10958  facndiv  11047  faclbnd  11049  bcval5  11071  hashen  11092  fihashdom  11112  hashunlem  11113  hashfacen  11146  zfz1isolemiso  11149  seq3coll  11152  ccatsymb  11228  ccatrn  11235  ccatw2s1p2  11272  swrdccatin1  11355  swrdccatin2  11359  swrdccat3b  11370  caucvgre  11604  resqrexlemlo  11636  cau3lem  11737  qdenre  11825  rexico  11844  fimaxre2  11850  2zinfmin  11866  xrmaxiflemcl  11868  xrmaxifle  11869  xrmaxiflemcom  11872  2clim  11924  cn1lem  11937  climsqz  11958  climsqz2  11959  climcau  11970  sumrbdclem  12001  summodclem2a  12005  fsum3  12011  fsumcl2lem  12022  fsumadd  12030  sumsnf  12033  fsum2dlemstep  12058  fisum0diag2  12071  fsummulc2  12072  mertenslemub  12158  mertenslemi1  12159  mertensabs  12161  ntrivcvgap  12172  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  prodmodc  12202  prod1dc  12210  prodsnf  12216  fprod2dlemstep  12246  efaddlem  12298  tanaddaplem  12362  zdvdsdc  12436  dvdseq  12472  dvdsext  12479  odd2np1  12497  sqoddm1div8z  12510  nno  12530  dfgcd3  12644  nninfctlemfo  12674  dvdslcm  12704  lcmneg  12709  lcmgcdlem  12712  ncoprmgcdne1b  12724  qredeq  12731  qredeu  12732  divgcdcoprm0  12736  exprmfct  12773  prmdvdsfz  12774  isprm5  12777  rpexp1i  12789  sqrt2irr  12797  nonsq  12842  eulerthlemrprm  12864  eulerthlema  12865  phisum  12876  modprmn0modprm0  12892  pclemdc  12924  pcz  12968  pcmpt  12979  fldivp1  12984  pcfac  12986  expnprm  12989  oddprmdvds  12990  prmpwdvds  12991  infpnlem1  12995  1arith  13003  4sqlem2  13025  4sqlemafi  13031  4sqleminfi  13033  4sqexercise2  13035  4sqlemsdc  13036  ctinfom  13112  enctlem  13116  nninfdclemlt  13135  setsfun  13180  setsfun0  13181  setscom  13185  gsumfzval  13537  mndissubm  13621  resmhm  13633  resmhm2  13634  mhmco  13636  gsumfzz  13641  gsumwsubmcl  13642  gsumwmhm  13644  dfgrp2  13673  isgrpinv  13700  mulgval  13772  mulgnnp1  13780  mulgz  13800  grpissubg  13844  resghm  13910  qusecsub  13981  isrng  14011  lmodfopne  14405  dflidl2rng  14560  gsumfzfsumlemm  14666  mulgrhm2  14689  znidomb  14737  znunit  14738  psrbaglesuppg  14751  psrbagfi  14753  tgdom  14866  ssrest  14976  cnfval  14988  cnpfval  14989  cnpval  14992  iscnp3  14997  ssidcn  15004  cnpnei  15013  cnntr  15019  cncnp  15024  cnptopresti  15032  tx1cn  15063  upxp  15066  imasnopn  15093  bdmet  15296  metcnp  15306  ivthinclemlr  15431  ivthinclemur  15433  ivthinc  15437  dvrecap  15507  dvmptfsum  15519  elply2  15529  plymullem1  15542  plycolemc  15552  plycjlemc  15554  dvply1  15559  pilem3  15577  relogeftb  15659  logbgcd1irr  15761  mpodvdsmulf1o  15787  mersenne  15794  lgslem4  15805  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsmod  15828  lgsdir2lem4  15833  lgsdinn0  15850  lgsquad2lem2  15884  lgsquad3  15886  2lgslem1c  15892  2sqlem6  15922  2sqlem7  15923  isupgren  16019  wrdupgren  16020  isumgren  16029  wrdumgren  16030  isuspgren  16081  isusgren  16082  clwwlkext2edg  16346  clwwlknonex2  16363  depindlem3  16432  2omap  16698  pw1map  16700  nnsf  16714  peano4nninf  16715  nninfalllem1  16717  nninfsellemqall  16724  nninfsellemeqinf  16725  nninffeq  16729  exmidsbthrlem  16733  isomninnlem  16745  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768