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  529  simprll  537  simprlr  538  elxp5  5217  f1oprg  5619  elovmporab1w  6212  cnvf1olem  6376  tfrcl  6516  nnaordi  6662  swoer  6716  0er  6722  pw2f1odclem  7003  mapxpen  7017  fict  7038  dif1enen  7050  php5fin  7052  fin0  7055  fin0or  7056  diffisn  7063  infnfi  7065  unsnfi  7092  fidcenumlemrk  7132  sbthlemi8  7142  fiuni  7156  supmoti  7171  eldju2ndl  7250  eldju2ndr  7251  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  nninfninc  7301  nninfwlpor  7352  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  enq0sym  7630  nqnq0pi  7636  addlocpr  7734  nqprl  7749  addnqprlemrl  7755  addnqprlemru  7756  mulnqprlemrl  7771  mulnqprlemru  7772  archpr  7841  cauappcvgprlemloc  7850  cauappcvgprlemladdfl  7853  archrecpr  7862  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemdisj  7900  caucvgprprlemloc  7901  suplocexprlemmu  7916  suplocexprlemdisj  7918  mulcmpblnrlemg  7938  caucvgsrlemgt1  7993  axarch  8089  axcaucvglemres  8097  cnegexlem2  8333  mulge0  8777  divdivap1  8881  divdivap2  8882  conjmulap  8887  ltdivmul  9034  nn0ge0div  9545  peano2uz2  9565  peano5uzti  9566  eluzp1m1  9758  xleadd1a  10081  iooshf  10160  divelunit  10210  eluzgtdifelfzo  10415  zsupcllemex  10462  ioom  10492  modqcyc2  10594  modaddmodup  10621  uzennn  10670  seq3fveq2  10709  seqfveq2g  10711  seq3id2  10760  seqfeq3  10763  expineg2  10782  mulexpzap  10813  leexp2r  10827  expnlbnd2  10899  hashfacen  11071  wrdred1hash  11128  ccatsymb  11150  swrdwrdsymbg  11212  swrdsb0eq  11213  ccatpfx  11249  swrdswrd  11253  wrdind  11270  wrd2ind  11271  swrdccatin1  11273  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  resqrexlemp1rp  11533  resqrexlemfp1  11536  negfi  11755  climcaucn  11878  fsum3cvg3  11923  fsum2dlemstep  11961  mptfzshft  11969  expcnvre  12030  fprodrev  12146  fprod2dlemstep  12149  moddvds  12326  dvdsflip  12378  addmodlteqALT  12386  nn0o  12434  dfgcd2  12551  lcmgcdlem  12615  cncongr1  12641  prmind2  12658  isprm5lem  12679  isprm6  12685  cncongrprm  12695  oddpwdclemdc  12711  sqrt2irrap  12718  hashdvds  12759  crth  12762  prmdiveq  12774  hashgcdlem  12776  hashgcdeq  12778  pclem0  12825  pclemub  12826  pcprendvds2  12830  pcmul  12840  pcexp  12848  pcneg  12864  pc2dvds  12869  pcmpt  12882  prmpwdvds  12894  pockthg  12896  1arith  12906  4sqlem2  12928  4sqlemafi  12934  4sqlem11  12940  ennnfonelemex  13001  setscom  13088  subsubm  13532  insubm  13534  isgrpinv  13603  subsubg  13750  subsubrng  14194  subsubrg  14225  islss4  14362  znf1o  14631  znidomb  14638  tgcl  14754  lmbr2  14904  txcn  14965  txdis1cn  14968  txlm  14969  hmeoimaf1o  15004  txhmeo  15009  bl2in  15093  blssps  15117  blss  15118  blssexps  15119  blssex  15120  bdxmet  15191  xmetxp  15197  xmetxpbl  15198  xmettx  15200  metcnp3  15201  metcnpi3  15207  dedekindicc  15323  ivthdichlem  15341  limcimolemlt  15354  dvmptfsum  15415  rprelogbmul  15645  logbgcd1irr  15657  mpodvdsmulf1o  15680  lgsne0  15733  gausslemma2dlem1a  15753  lgseisenlem2  15766  lgsquadlemsfi  15770  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem2  15777  2sqlem8  15818  uspgredg2vlem  16034  iswlkg  16075  wlkl1loop  16104  upgriswlkdc  16106  clwwlkccatlem  16143  clwwlkn1loopb  16162  2omap  16446  qdencn  16483  trilpolemlt1  16497