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  5119  f1oprg  5507  cnvf1olem  6227  tfrcl  6367  nnaordi  6511  swoer  6565  0er  6571  mapxpen  6850  fict  6870  dif1enen  6882  php5fin  6884  fin0  6887  fin0or  6888  diffisn  6895  infnfi  6897  unsnfi  6920  fidcenumlemrk  6955  sbthlemi8  6965  fiuni  6979  supmoti  6994  eldju2ndl  7073  eldju2ndr  7074  omp1eomlem  7095  difinfsnlem  7100  ctmlemr  7109  nninfwlpor  7174  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  enq0sym  7433  nqnq0pi  7439  addlocpr  7537  nqprl  7552  addnqprlemrl  7558  addnqprlemru  7559  mulnqprlemrl  7574  mulnqprlemru  7575  archpr  7644  cauappcvgprlemloc  7653  cauappcvgprlemladdfl  7656  archrecpr  7665  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprprlemml  7695  caucvgprprlemopl  7698  caucvgprprlemdisj  7703  caucvgprprlemloc  7704  suplocexprlemmu  7719  suplocexprlemdisj  7721  mulcmpblnrlemg  7741  caucvgsrlemgt1  7796  axarch  7892  axcaucvglemres  7900  cnegexlem2  8135  mulge0  8578  divdivap1  8682  divdivap2  8683  conjmulap  8688  ltdivmul  8835  nn0ge0div  9342  peano2uz2  9362  peano5uzti  9363  eluzp1m1  9553  xleadd1a  9875  iooshf  9954  divelunit  10004  eluzgtdifelfzo  10199  ioom  10263  modqcyc2  10362  modaddmodup  10389  uzennn  10438  seq3fveq2  10471  seq3id2  10511  seqfeq3  10514  expineg2  10531  mulexpzap  10562  leexp2r  10576  expnlbnd2  10648  hashfacen  10818  resqrexlemp1rp  11017  resqrexlemfp1  11020  negfi  11238  climcaucn  11361  fsum3cvg3  11406  fsum2dlemstep  11444  mptfzshft  11452  expcnvre  11513  fprodrev  11629  fprod2dlemstep  11632  moddvds  11808  dvdsflip  11859  addmodlteqALT  11867  nn0o  11914  zsupcllemex  11949  dfgcd2  12017  lcmgcdlem  12079  cncongr1  12105  prmind2  12122  isprm5lem  12143  isprm6  12149  cncongrprm  12159  oddpwdclemdc  12175  sqrt2irrap  12182  hashdvds  12223  crth  12226  prmdiveq  12238  hashgcdlem  12240  hashgcdeq  12241  pclem0  12288  pclemub  12289  pcprendvds2  12293  pcmul  12303  pcexp  12311  pcneg  12326  pc2dvds  12331  pcmpt  12343  prmpwdvds  12355  pockthg  12357  1arith  12367  4sqlem2  12389  ennnfonelemex  12417  setscom  12504  insubm  12877  isgrpinv  12931  subsubg  13062  subsubrg  13371  islss4  13474  tgcl  13649  lmbr2  13799  txcn  13860  txdis1cn  13863  txlm  13864  hmeoimaf1o  13899  txhmeo  13904  bl2in  13988  blssps  14012  blss  14013  blssexps  14014  blssex  14015  bdxmet  14086  xmetxp  14092  xmetxpbl  14093  xmettx  14095  metcnp3  14096  metcnpi3  14102  dedekindicc  14196  limcimolemlt  14218  rprelogbmul  14458  logbgcd1irr  14470  lgsne0  14524  lgseisenlem2  14536  2sqlem8  14555  qdencn  14860  trilpolemlt1  14874