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  533  simprrl  541  simprrr  542  dn1dc  969  prneimg  3878  f1oprg  5660  fvco4  5749  nnsucuniel  6728  modom  7061  mapen  7099  mapxpen  7101  mapunen  7104  fidceq  7124  fidifsnen  7125  php5fin  7139  findcard2d  7148  findcard2sd  7149  diffisn  7150  fidcenumlemr  7225  supmoti  7284  djuf1olem  7344  nninfwlpor  7465  exmidfodomrlemim  7504  cc4f  7583  cc4n  7585  subhalfnqq  7729  nqnq0pi  7753  genprndl  7836  genprndu  7837  addlocpr  7851  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  mullocpr  7886  mulnqprlemrl  7888  mulnqprlemru  7889  ltaprlem  7933  aptiprleml  7954  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemladdfu  7992  caucvgprprlemloc  8018  suplocexprlemrl  8032  suplocexprlemru  8034  mulcmpblnrlemg  8055  recexgt0sr  8088  pitonn  8163  rereceu  8204  rimul  8859  receuap  8943  peano5uzti  9686  iooshf  10285  seq3fveq2  10837  seqfveq2g  10839  seq3id2  10888  seqfeq3  10891  expcl2lemap  10913  mulexpzap  10941  expnlbnd2  11027  hashfacen  11208  fstwrdne0  11264  swrdsb0eq  11357  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  absexpzap  11765  fsumf1o  12076  fisum0diag2  12133  fsummulc2  12134  fprodmul  12277  fprodrev  12305  moddvds  12485  dvdsflip  12537  dfgcd3  12706  dfgcd2  12710  lcmgcdlem  12774  cncongr1  12800  hashgcdlem  12935  phisum  12938  pcval  12994  pcqcl  13004  pcid  13022  pcneg  13023  prmpwdvds  13053  pockthg  13055  4sqlem2  13087  4sqlem11  13099  setscom  13252  qusval  13536  mulgdirlem  13870  mulgass  13876  0nsg  13931  ghmmulg  13973  islmodd  14441  lmodvsmmulgdi  14471  islss3  14527  znf1o  14799  tgcl  14929  epttop  14955  cnpnei  15084  txcn  15140  txdis1cn  15143  imasnopn  15164  hmeoimaf1o  15179  txhmeo  15184  metss2lem  15362  bdxmet  15366  bdmopn  15369  metrest  15371  xmetxp  15372  metcnp  15377  dvmptfsum  15590  plycn  15627  dvply2g  15631  rprelogbmul  15820  logbgcd1irr  15832  mpodvdsmulf1o  15858  gausslemma2dlem1a  15931  lgseisenlem2  15944  lgsquadlemsfi  15948  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  subgrprop3  16257  subupgr  16268  wlkl1loop  16353  clwwlknp  16412