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  3829  f1oprg  5590  fvco4  5676  nnsucuniel  6606  mapen  6970  mapxpen  6972  fidceq  6994  fidifsnen  6995  php5fin  7007  findcard2d  7016  findcard2sd  7017  diffisn  7018  fidcenumlemr  7085  supmoti  7123  djuf1olem  7183  nninfwlpor  7304  exmidfodomrlemim  7342  cc4f  7418  cc4n  7420  subhalfnqq  7564  nqnq0pi  7588  genprndl  7671  genprndu  7672  addlocpr  7686  nqprl  7701  nqpru  7702  addnqprlemrl  7707  addnqprlemru  7708  mullocpr  7721  mulnqprlemrl  7723  mulnqprlemru  7724  ltaprlem  7768  aptiprleml  7789  cauappcvgprlemladdfu  7804  cauappcvgprlemladdfl  7805  caucvgprlemladdfu  7827  caucvgprprlemloc  7853  suplocexprlemrl  7867  suplocexprlemru  7869  mulcmpblnrlemg  7890  recexgt0sr  7923  pitonn  7998  rereceu  8039  rimul  8695  receuap  8779  peano5uzti  9518  iooshf  10111  seq3fveq2  10659  seqfveq2g  10661  seq3id2  10710  seqfeq3  10713  expcl2lemap  10735  mulexpzap  10763  expnlbnd2  10849  hashfacen  11020  fstwrdne0  11072  swrdsb0eq  11158  swrdswrd  11198  wrd2ind  11216  swrdccatin1  11218  pfxccatin12  11226  pfxccat3  11227  swrdccat  11228  absexpzap  11552  fsumf1o  11862  fisum0diag2  11919  fsummulc2  11920  fprodmul  12063  fprodrev  12091  moddvds  12271  dvdsflip  12323  dfgcd3  12492  dfgcd2  12496  lcmgcdlem  12560  cncongr1  12586  hashgcdlem  12721  phisum  12724  pcval  12780  pcqcl  12790  pcid  12808  pcneg  12809  prmpwdvds  12839  pockthg  12841  4sqlem2  12873  4sqlem11  12885  setscom  13033  qusval  13316  mulgdirlem  13650  mulgass  13656  0nsg  13711  ghmmulg  13753  islmodd  14216  lmodvsmmulgdi  14246  islss3  14302  znf1o  14574  tgcl  14697  epttop  14723  cnpnei  14852  txcn  14908  txdis1cn  14911  imasnopn  14932  hmeoimaf1o  14947  txhmeo  14952  metss2lem  15130  bdxmet  15134  bdmopn  15137  metrest  15139  xmetxp  15140  metcnp  15145  dvmptfsum  15358  plycn  15395  dvply2g  15399  rprelogbmul  15588  logbgcd1irr  15600  mpodvdsmulf1o  15623  gausslemma2dlem1a  15696  lgseisenlem2  15709  lgsquadlemsfi  15713  lgsquadlem1  15715  lgsquadlem2  15716  lgsquadlem3  15717