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  902  prneimg  3592  f1oprg  5243  fvco4  5321  nnsucuniel  6188  mapen  6492  mapxpen  6494  fidceq  6515  fidifsnen  6516  php5fin  6528  findcard2d  6537  findcard2sd  6538  diffisn  6539  supmoti  6595  djuf1olem  6652  exmidfodomrlemim  6730  subhalfnqq  6876  nqnq0pi  6900  genprndl  6983  genprndu  6984  addlocpr  6998  nqprl  7013  nqpru  7014  addnqprlemrl  7019  addnqprlemru  7020  mullocpr  7033  mulnqprlemrl  7035  mulnqprlemru  7036  ltaprlem  7080  aptiprleml  7101  cauappcvgprlemladdfu  7116  cauappcvgprlemladdfl  7117  caucvgprlemladdfu  7139  caucvgprprlemloc  7165  mulcmpblnrlemg  7189  recexgt0sr  7222  pitonn  7288  rereceu  7327  rimul  7962  receuap  8036  peano5uzti  8750  iooshf  9265  iseqfveq2  9763  iseqid2  9783  expcl2lemap  9804  mulexpzap  9832  expnlbnd2  9914  hashfacen  10075  absexpzap  10340  moddvds  10585  dvdsflip  10632  dfgcd3  10779  dfgcd2  10783  lcmgcdlem  10839  cncongr1  10865  hashgcdlem  10983