Theorem ad2antrl 473

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 270	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 271	1 |- ( ( ch /\ ( ph /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  simprl  497  simprll  503  simprlr  504  elxp5  4829  f1oprg  5188  cnvf1olem  5865  nnaordi  6104  swoer  6157  0er  6163  php5fin  6366  fin0  6369  fin0or  6370  diffisn  6377  unsnfi  6384  supmoti  6406  enq0sym  6622  nqnq0pi  6628  addlocpr  6726  nqprl  6741  addnqprlemrl  6747  addnqprlemru  6748  mulnqprlemrl  6763  mulnqprlemru  6764  archpr  6833  cauappcvgprlemloc  6842  cauappcvgprlemladdfl  6845  archrecpr  6854  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  mulcmpblnrlemg  6917  caucvgsrlemgt1  6971  axarch  7057  axcaucvglemres  7065  cnegexlem2  7284  mulge0  7719  divdivap1  7811  divdivap2  7812  conjmulap  7817  ltdivmul  7954  nn0ge0div  8434  peano2uz2  8454  peano5uzti  8455  eluzp1m1  8642  iooshf  8975  divelunit  9024  eluzgtdifelfzo  9206  ioom  9269  modqcyc2  9362  modaddmodup  9389  iseqval  9440  iseqfveq2  9448  expineg2  9485  mulexpzap  9516  leexp2r  9530  expnlbnd2  9598  resqrexlemp1rp  9892  resqrexlemfp1  9895  negfi  10110  climcaucn  10188  moddvds  10204  dvdsflip  10251  addmodlteqALT  10259  nn0o  10307  zsupcllemex  10342  dfgcd2  10403  lcmgcdlem  10459  cncongr1  10485  prmind2  10502  isprm6  10526  cncongrprm  10536  oddpwdclemdc  10551  sqrt2irrap  10558  qdencn  10785