Theorem ad2antll 475

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  499  simprrl  506  simprrr  507  dn1dc  904  prneimg  3603  f1oprg  5260  fvco4  5341  nnsucuniel  6212  mapen  6516  mapxpen  6518  fidceq  6539  fidifsnen  6540  php5fin  6552  findcard2d  6561  findcard2sd  6562  diffisn  6563  supmoti  6635  djuf1olem  6692  exmidfodomrlemim  6774  subhalfnqq  6920  nqnq0pi  6944  genprndl  7027  genprndu  7028  addlocpr  7042  nqprl  7057  nqpru  7058  addnqprlemrl  7063  addnqprlemru  7064  mullocpr  7077  mulnqprlemrl  7079  mulnqprlemru  7080  ltaprlem  7124  aptiprleml  7145  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  caucvgprlemladdfu  7183  caucvgprprlemloc  7209  mulcmpblnrlemg  7233  recexgt0sr  7266  pitonn  7332  rereceu  7371  rimul  8006  receuap  8080  peano5uzti  8790  iooshf  9305  iseqfveq2  9806  iseqid2  9847  expcl2lemap  9869  mulexpzap  9897  expnlbnd2  9979  hashfacen  10141  absexpzap  10412  fsumf1o  10673  moddvds  10711  dvdsflip  10758  dfgcd3  10905  dfgcd2  10909  lcmgcdlem  10965  cncongr1  10991  hashgcdlem  11109