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  960  prneimg  3776  f1oprg  5507  fvco4  5590  nnsucuniel  6498  mapen  6848  mapxpen  6850  fidceq  6871  fidifsnen  6872  php5fin  6884  findcard2d  6893  findcard2sd  6894  diffisn  6895  fidcenumlemr  6956  supmoti  6994  djuf1olem  7054  nninfwlpor  7174  exmidfodomrlemim  7202  cc4f  7270  cc4n  7272  subhalfnqq  7415  nqnq0pi  7439  genprndl  7522  genprndu  7523  addlocpr  7537  nqprl  7552  nqpru  7553  addnqprlemrl  7558  addnqprlemru  7559  mullocpr  7572  mulnqprlemrl  7574  mulnqprlemru  7575  ltaprlem  7619  aptiprleml  7640  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  caucvgprlemladdfu  7678  caucvgprprlemloc  7704  suplocexprlemrl  7718  suplocexprlemru  7720  mulcmpblnrlemg  7741  recexgt0sr  7774  pitonn  7849  rereceu  7890  rimul  8544  receuap  8628  peano5uzti  9363  iooshf  9954  seq3fveq2  10471  seq3id2  10511  seqfeq3  10514  expcl2lemap  10534  mulexpzap  10562  expnlbnd2  10648  hashfacen  10818  absexpzap  11091  fsumf1o  11400  fisum0diag2  11457  fsummulc2  11458  fprodmul  11601  fprodrev  11629  moddvds  11808  dvdsflip  11859  dfgcd3  12013  dfgcd2  12017  lcmgcdlem  12079  cncongr1  12105  hashgcdlem  12240  phisum  12242  pcval  12298  pcqcl  12308  pcid  12325  pcneg  12326  prmpwdvds  12355  pockthg  12357  4sqlem2  12389  setscom  12504  qusval  12749  mulgdirlem  13019  mulgass  13025  0nsg  13079  islmodd  13388  lmodvsmmulgdi  13418  islss3  13471  tgcl  13603  epttop  13629  cnpnei  13758  txcn  13814  txdis1cn  13817  imasnopn  13838  hmeoimaf1o  13853  txhmeo  13858  metss2lem  14036  bdxmet  14040  bdmopn  14043  metrest  14045  xmetxp  14046  metcnp  14051  rprelogbmul  14412  logbgcd1irr  14424  lgseisenlem2  14490