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  3801  f1oprg  5545  fvco4  5630  nnsucuniel  6550  mapen  6904  mapxpen  6906  fidceq  6927  fidifsnen  6928  php5fin  6940  findcard2d  6949  findcard2sd  6950  diffisn  6951  fidcenumlemr  7016  supmoti  7054  djuf1olem  7114  nninfwlpor  7235  exmidfodomrlemim  7263  cc4f  7331  cc4n  7333  subhalfnqq  7476  nqnq0pi  7500  genprndl  7583  genprndu  7584  addlocpr  7598  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  mullocpr  7633  mulnqprlemrl  7635  mulnqprlemru  7636  ltaprlem  7680  aptiprleml  7701  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemladdfu  7739  caucvgprprlemloc  7765  suplocexprlemrl  7779  suplocexprlemru  7781  mulcmpblnrlemg  7802  recexgt0sr  7835  pitonn  7910  rereceu  7951  rimul  8606  receuap  8690  peano5uzti  9428  iooshf  10021  seq3fveq2  10549  seqfveq2g  10551  seq3id2  10600  seqfeq3  10603  expcl2lemap  10625  mulexpzap  10653  expnlbnd2  10739  hashfacen  10910  fstwrdne0  10956  absexpzap  11227  fsumf1o  11536  fisum0diag2  11593  fsummulc2  11594  fprodmul  11737  fprodrev  11765  moddvds  11945  dvdsflip  11996  dfgcd3  12150  dfgcd2  12154  lcmgcdlem  12218  cncongr1  12244  hashgcdlem  12379  phisum  12381  pcval  12437  pcqcl  12447  pcid  12465  pcneg  12466  prmpwdvds  12496  pockthg  12498  4sqlem2  12530  4sqlem11  12542  setscom  12661  qusval  12909  mulgdirlem  13226  mulgass  13232  0nsg  13287  ghmmulg  13329  islmodd  13792  lmodvsmmulgdi  13822  islss3  13878  znf1o  14150  tgcl  14243  epttop  14269  cnpnei  14398  txcn  14454  txdis1cn  14457  imasnopn  14478  hmeoimaf1o  14493  txhmeo  14498  metss2lem  14676  bdxmet  14680  bdmopn  14683  metrest  14685  xmetxp  14686  metcnp  14691  dvmptfsum  14904  plycn  14940  rprelogbmul  15128  logbgcd1irr  15140  gausslemma2dlem1a  15215  lgseisenlem2  15228  lgsquadlemsfi  15232  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236