Theorem ad2antll 474

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

Hypothesis

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

Assertion

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

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantl 271	. 2 |- ( ( th /\ ph ) -> ps )
3	2	adantl 271	1 |- ( ( ch /\ ( th /\ ph ) ) -> 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:  simprr  498  simprrl  505  simprrr  506  dn1dc  901  prneimg  3566  f1oprg  5188  fidceq  6354  fidifsnen  6355  php5fin  6366  findcard2d  6375  findcard2sd  6376  diffisn  6377  supmoti  6406  subhalfnqq  6604  nqnq0pi  6628  genprndl  6711  genprndu  6712  addlocpr  6726  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  ltaprlem  6808  aptiprleml  6829  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  caucvgprlemladdfu  6867  caucvgprprlemloc  6893  mulcmpblnrlemg  6917  recexgt0sr  6950  pitonn  7016  rereceu  7055  rimul  7685  receuap  7759  peano5uzti  8455  iooshf  8975  iseqfveq2  9448  expcl2lemap  9488  mulexpzap  9516  expnlbnd2  9598  absexpzap  9966  moddvds  10204  dvdsflip  10251  dfgcd3  10399  dfgcd2  10403  lcmgcdlem  10459  cncongr1  10485