Theorem ad2antll 488

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simprr  527  simprrl  534  simprrr  535  dn1dc  955  prneimg  3759  f1oprg  5484  fvco4  5566  nnsucuniel  6471  mapen  6820  mapxpen  6822  fidceq  6843  fidifsnen  6844  php5fin  6856  findcard2d  6865  findcard2sd  6866  diffisn  6867  fidcenumlemr  6928  supmoti  6966  djuf1olem  7026  exmidfodomrlemim  7165  cc4f  7218  cc4n  7220  subhalfnqq  7363  nqnq0pi  7387  genprndl  7470  genprndu  7471  addlocpr  7485  nqprl  7500  nqpru  7501  addnqprlemrl  7506  addnqprlemru  7507  mullocpr  7520  mulnqprlemrl  7522  mulnqprlemru  7523  ltaprlem  7567  aptiprleml  7588  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  caucvgprlemladdfu  7626  caucvgprprlemloc  7652  suplocexprlemrl  7666  suplocexprlemru  7668  mulcmpblnrlemg  7689  recexgt0sr  7722  pitonn  7797  rereceu  7838  rimul  8491  receuap  8574  peano5uzti  9307  iooshf  9896  seq3fveq2  10412  seq3id2  10452  seqfeq3  10455  expcl2lemap  10475  mulexpzap  10503  expnlbnd2  10588  hashfacen  10758  absexpzap  11031  fsumf1o  11340  fisum0diag2  11397  fsummulc2  11398  fprodmul  11541  fprodrev  11569  moddvds  11748  dvdsflip  11798  dfgcd3  11952  dfgcd2  11956  lcmgcdlem  12018  cncongr1  12044  hashgcdlem  12179  phisum  12181  pcval  12237  pcqcl  12247  pcid  12264  pcneg  12265  prmpwdvds  12294  pockthg  12296  4sqlem2  12328  setscom  12443  tgcl  12779  epttop  12805  cnpnei  12934  txcn  12990  txdis1cn  12993  imasnopn  13014  hmeoimaf1o  13029  txhmeo  13034  metss2lem  13212  bdxmet  13216  bdmopn  13219  metrest  13221  xmetxp  13222  metcnp  13227  rprelogbmul  13588  logbgcd1irr  13600