Theorem ad2antll 491

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  simprr  531  simprrl  539  simprrr  540  dn1dc  966  prneimg  3852  f1oprg  5619  fvco4  5708  nnsucuniel  6649  mapen  7015  mapxpen  7017  fidceq  7039  fidifsnen  7040  php5fin  7052  findcard2d  7061  findcard2sd  7062  diffisn  7063  fidcenumlemr  7133  supmoti  7171  djuf1olem  7231  nninfwlpor  7352  exmidfodomrlemim  7390  cc4f  7466  cc4n  7468  subhalfnqq  7612  nqnq0pi  7636  genprndl  7719  genprndu  7720  addlocpr  7734  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  mullocpr  7769  mulnqprlemrl  7771  mulnqprlemru  7772  ltaprlem  7816  aptiprleml  7837  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemladdfu  7875  caucvgprprlemloc  7901  suplocexprlemrl  7915  suplocexprlemru  7917  mulcmpblnrlemg  7938  recexgt0sr  7971  pitonn  8046  rereceu  8087  rimul  8743  receuap  8827  peano5uzti  9566  iooshf  10160  seq3fveq2  10709  seqfveq2g  10711  seq3id2  10760  seqfeq3  10763  expcl2lemap  10785  mulexpzap  10813  expnlbnd2  10899  hashfacen  11071  fstwrdne0  11124  swrdsb0eq  11213  swrdswrd  11253  wrd2ind  11271  swrdccatin1  11273  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  absexpzap  11607  fsumf1o  11917  fisum0diag2  11974  fsummulc2  11975  fprodmul  12118  fprodrev  12146  moddvds  12326  dvdsflip  12378  dfgcd3  12547  dfgcd2  12551  lcmgcdlem  12615  cncongr1  12641  hashgcdlem  12776  phisum  12779  pcval  12835  pcqcl  12845  pcid  12863  pcneg  12864  prmpwdvds  12894  pockthg  12896  4sqlem2  12928  4sqlem11  12940  setscom  13088  qusval  13372  mulgdirlem  13706  mulgass  13712  0nsg  13767  ghmmulg  13809  islmodd  14273  lmodvsmmulgdi  14303  islss3  14359  znf1o  14631  tgcl  14754  epttop  14780  cnpnei  14909  txcn  14965  txdis1cn  14968  imasnopn  14989  hmeoimaf1o  15004  txhmeo  15009  metss2lem  15187  bdxmet  15191  bdmopn  15194  metrest  15196  xmetxp  15197  metcnp  15202  dvmptfsum  15415  plycn  15452  dvply2g  15456  rprelogbmul  15645  logbgcd1irr  15657  mpodvdsmulf1o  15680  gausslemma2dlem1a  15753  lgseisenlem2  15766  lgsquadlemsfi  15770  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  wlkl1loop  16104  clwwlknp  16159