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  963  prneimg  3815  f1oprg  5568  fvco4  5653  nnsucuniel  6583  mapen  6945  mapxpen  6947  fidceq  6968  fidifsnen  6969  php5fin  6981  findcard2d  6990  findcard2sd  6991  diffisn  6992  fidcenumlemr  7059  supmoti  7097  djuf1olem  7157  nninfwlpor  7278  exmidfodomrlemim  7311  cc4f  7383  cc4n  7385  subhalfnqq  7529  nqnq0pi  7553  genprndl  7636  genprndu  7637  addlocpr  7651  nqprl  7666  nqpru  7667  addnqprlemrl  7672  addnqprlemru  7673  mullocpr  7686  mulnqprlemrl  7688  mulnqprlemru  7689  ltaprlem  7733  aptiprleml  7754  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  caucvgprlemladdfu  7792  caucvgprprlemloc  7818  suplocexprlemrl  7832  suplocexprlemru  7834  mulcmpblnrlemg  7855  recexgt0sr  7888  pitonn  7963  rereceu  8004  rimul  8660  receuap  8744  peano5uzti  9483  iooshf  10076  seq3fveq2  10622  seqfveq2g  10624  seq3id2  10673  seqfeq3  10676  expcl2lemap  10698  mulexpzap  10726  expnlbnd2  10812  hashfacen  10983  fstwrdne0  11035  swrdsb0eq  11121  absexpzap  11424  fsumf1o  11734  fisum0diag2  11791  fsummulc2  11792  fprodmul  11935  fprodrev  11963  moddvds  12143  dvdsflip  12195  dfgcd3  12364  dfgcd2  12368  lcmgcdlem  12432  cncongr1  12458  hashgcdlem  12593  phisum  12596  pcval  12652  pcqcl  12662  pcid  12680  pcneg  12681  prmpwdvds  12711  pockthg  12713  4sqlem2  12745  4sqlem11  12757  setscom  12905  qusval  13188  mulgdirlem  13522  mulgass  13528  0nsg  13583  ghmmulg  13625  islmodd  14088  lmodvsmmulgdi  14118  islss3  14174  znf1o  14446  tgcl  14569  epttop  14595  cnpnei  14724  txcn  14780  txdis1cn  14783  imasnopn  14804  hmeoimaf1o  14819  txhmeo  14824  metss2lem  15002  bdxmet  15006  bdmopn  15009  metrest  15011  xmetxp  15012  metcnp  15017  dvmptfsum  15230  plycn  15267  dvply2g  15271  rprelogbmul  15460  logbgcd1irr  15472  mpodvdsmulf1o  15495  gausslemma2dlem1a  15568  lgseisenlem2  15581  lgsquadlemsfi  15585  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589