Theorem ad2antll 495

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  537  simprrl  545  simprrr  546  dn1dc  973  prneimg  3894  f1oprg  5680  fvco4  5771  nnsucuniel  6758  modom  7098  mapen  7136  mapxpen  7138  mapunen  7141  fidceq  7161  fidifsnen  7162  php5fin  7176  findcard2d  7185  findcard2sd  7186  diffisn  7187  fidcenumlemr  7262  supmoti  7323  djuf1olem  7383  nninfwlpor  7504  exmidfodomrlemim  7543  cc4f  7625  cc4n  7627  subhalfnqq  7771  nqnq0pi  7795  genprndl  7878  genprndu  7879  addlocpr  7893  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  mullocpr  7928  mulnqprlemrl  7930  mulnqprlemru  7931  ltaprlem  7975  aptiprleml  7996  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemladdfu  8034  caucvgprprlemloc  8060  suplocexprlemrl  8074  suplocexprlemru  8076  mulcmpblnrlemg  8097  recexgt0sr  8130  pitonn  8205  rereceu  8246  rimul  8903  receuap  8989  peano5uzti  9733  iooshf  10333  seq3fveq2  10890  seqfveq2g  10892  seq3id2  10941  seqfeq3  10944  expcl2lemap  10966  mulexpzap  10994  expnlbnd2  11081  hashfacen  11262  hashf1lem1  11263  fstwrdne0  11322  swrdsb0eq  11415  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  absexpzap  11824  fsumf1o  12135  fisum0diag2  12192  fsummulc2  12193  fprodmul  12336  fprodrev  12364  moddvds  12544  dvdsflip  12596  dfgcd3  12765  dfgcd2  12769  lcmgcdlem  12833  cncongr1  12859  hashgcdlem  12994  phisum  12997  pcval  13053  pcqcl  13063  pcid  13081  pcneg  13082  prmpwdvds  13112  pockthg  13114  4sqlem2  13146  4sqlem11  13158  ballotfilemsf1o  13235  setscom  13370  qusval  13621  mulgdirlem  13933  mulgass  13939  0nsg  13994  ghmmulg  14036  islmodd  14602  lmodvsmmulgdi  14632  islss3  14688  znf1o  14958  tgcl  15088  epttop  15114  cnpnei  15243  txcn  15299  txdis1cn  15302  imasnopn  15323  hmeoimaf1o  15338  txhmeo  15343  metss2lem  15521  bdxmet  15525  bdmopn  15528  metrest  15530  xmetxp  15531  metcnp  15536  dvmptfsum  15749  plycn  15786  dvply2g  15790  rprelogbmul  15980  logbgcd1irr  15992  mpodvdsmulf1o  16018  gausslemma2dlem1a  16091  lgseisenlem2  16104  lgsquadlemsfi  16108  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  subgrprop3  16417  subupgr  16428  wlkl1loop  16513  clwwlknp  16572