Theorem ad2antrl 490

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

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

Assertion

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

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 277	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:  simprl  531  simprll  539  simprlr  540  elxp5  5232  f1oprg  5638  elovmporab1w  6233  cnvf1olem  6398  ressuppss  6432  tfrcl  6573  nnaordi  6719  swoer  6773  0er  6779  modom  7037  pw2f1odclem  7063  mapxpen  7077  fict  7098  dif1enen  7112  php5fin  7114  fin0  7117  fin0or  7118  diffisn  7125  infnfi  7127  unsnfi  7154  fidcenumlemrk  7196  sbthlemi8  7206  fiuni  7220  supmoti  7235  eldju2ndl  7314  eldju2ndr  7315  omp1eomlem  7336  difinfsnlem  7341  ctmlemr  7350  nninfninc  7365  nninfwlpor  7416  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  enq0sym  7695  nqnq0pi  7701  addlocpr  7799  nqprl  7814  addnqprlemrl  7820  addnqprlemru  7821  mulnqprlemrl  7836  mulnqprlemru  7837  archpr  7906  cauappcvgprlemloc  7915  cauappcvgprlemladdfl  7918  archrecpr  7927  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  suplocexprlemmu  7981  suplocexprlemdisj  7983  mulcmpblnrlemg  8003  caucvgsrlemgt1  8058  axarch  8154  axcaucvglemres  8162  cnegexlem2  8398  mulge0  8842  divdivap1  8946  divdivap2  8947  conjmulap  8952  ltdivmul  9099  nn0ge0div  9610  peano2uz2  9630  peano5uzti  9631  eluzp1m1  9823  xleadd1a  10151  iooshf  10230  divelunit  10280  eluzgtdifelfzo  10486  zsupcllemex  10534  ioom  10564  modqcyc2  10666  modaddmodup  10693  uzennn  10742  seq3fveq2  10781  seqfveq2g  10783  seq3id2  10832  seqfeq3  10835  expineg2  10854  mulexpzap  10885  leexp2r  10899  expnlbnd2  10971  hashfacen  11144  wrdred1hash  11204  ccatsymb  11226  swrdwrdsymbg  11292  swrdsb0eq  11293  ccatpfx  11329  swrdswrd  11333  wrdind  11350  wrd2ind  11351  swrdccatin1  11353  swrdccatin2  11357  pfxccatin12lem2  11359  pfxccatin12  11361  pfxccat3  11362  swrdccat  11363  resqrexlemp1rp  11627  resqrexlemfp1  11630  negfi  11849  climcaucn  11972  fsum3cvg3  12018  fsum2dlemstep  12056  mptfzshft  12064  expcnvre  12125  fprodrev  12241  fprod2dlemstep  12244  moddvds  12421  dvdsflip  12473  addmodlteqALT  12481  nn0o  12529  dfgcd2  12646  lcmgcdlem  12710  cncongr1  12736  prmind2  12753  isprm5lem  12774  isprm6  12780  cncongrprm  12790  oddpwdclemdc  12806  sqrt2irrap  12813  hashdvds  12854  crth  12857  prmdiveq  12869  hashgcdlem  12871  hashgcdeq  12873  pclem0  12920  pclemub  12921  pcprendvds2  12925  pcmul  12935  pcexp  12943  pcneg  12959  pc2dvds  12964  pcmpt  12977  prmpwdvds  12989  pockthg  12991  1arith  13001  4sqlem2  13023  4sqlemafi  13029  4sqlem11  13035  ennnfonelemex  13096  setscom  13183  subsubm  13627  insubm  13629  isgrpinv  13698  subsubg  13845  subsubrng  14290  subsubrg  14321  islss4  14458  znf1o  14727  znidomb  14734  tgcl  14855  lmbr2  15005  txcn  15066  txdis1cn  15069  txlm  15070  hmeoimaf1o  15105  txhmeo  15110  bl2in  15194  blssps  15218  blss  15219  blssexps  15220  blssex  15221  bdxmet  15292  xmetxp  15298  xmetxpbl  15299  xmettx  15301  metcnp3  15302  metcnpi3  15308  dedekindicc  15424  ivthdichlem  15442  limcimolemlt  15455  dvmptfsum  15516  rprelogbmul  15746  logbgcd1irr  15758  mpodvdsmulf1o  15784  lgsne0  15837  gausslemma2dlem1a  15857  lgseisenlem2  15870  lgsquadlemsfi  15874  lgsquadlem1  15876  lgsquadlem2  15877  lgsquadlem3  15878  lgsquad2lem2  15881  2sqlem8  15922  uspgredg2vlem  16141  subuhgr  16193  subupgr  16194  subumgr  16195  iswlkg  16250  wlkl1loop  16279  upgriswlkdc  16281  clwwlkccatlem  16321  clwwlkn1loopb  16341  clwwlknonex2e  16361  2omap  16695  qdencn  16735  trilpolemlt1  16753