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  962  prneimg  3804  f1oprg  5548  fvco4  5633  nnsucuniel  6553  mapen  6907  mapxpen  6909  fidceq  6930  fidifsnen  6931  php5fin  6943  findcard2d  6952  findcard2sd  6953  diffisn  6954  fidcenumlemr  7021  supmoti  7059  djuf1olem  7119  nninfwlpor  7240  exmidfodomrlemim  7268  cc4f  7336  cc4n  7338  subhalfnqq  7481  nqnq0pi  7505  genprndl  7588  genprndu  7589  addlocpr  7603  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  mullocpr  7638  mulnqprlemrl  7640  mulnqprlemru  7641  ltaprlem  7685  aptiprleml  7706  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemladdfu  7744  caucvgprprlemloc  7770  suplocexprlemrl  7784  suplocexprlemru  7786  mulcmpblnrlemg  7807  recexgt0sr  7840  pitonn  7915  rereceu  7956  rimul  8612  receuap  8696  peano5uzti  9434  iooshf  10027  seq3fveq2  10567  seqfveq2g  10569  seq3id2  10618  seqfeq3  10621  expcl2lemap  10643  mulexpzap  10671  expnlbnd2  10757  hashfacen  10928  fstwrdne0  10974  absexpzap  11245  fsumf1o  11555  fisum0diag2  11612  fsummulc2  11613  fprodmul  11756  fprodrev  11784  moddvds  11964  dvdsflip  12016  dfgcd3  12177  dfgcd2  12181  lcmgcdlem  12245  cncongr1  12271  hashgcdlem  12406  phisum  12409  pcval  12465  pcqcl  12475  pcid  12493  pcneg  12494  prmpwdvds  12524  pockthg  12526  4sqlem2  12558  4sqlem11  12570  setscom  12718  qusval  12966  mulgdirlem  13283  mulgass  13289  0nsg  13344  ghmmulg  13386  islmodd  13849  lmodvsmmulgdi  13879  islss3  13935  znf1o  14207  tgcl  14300  epttop  14326  cnpnei  14455  txcn  14511  txdis1cn  14514  imasnopn  14535  hmeoimaf1o  14550  txhmeo  14555  metss2lem  14733  bdxmet  14737  bdmopn  14740  metrest  14742  xmetxp  14743  metcnp  14748  dvmptfsum  14961  plycn  14998  dvply2g  15002  rprelogbmul  15191  logbgcd1irr  15203  mpodvdsmulf1o  15226  gausslemma2dlem1a  15299  lgseisenlem2  15312  lgsquadlemsfi  15316  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320