Theorem ad2antll 488

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 275	. 2 |- ( ( th /\ ph ) -> ps )
3	2	adantl 275	1 |- ( ( ch /\ ( th /\ ph ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simprr  527  simprrl  534  simprrr  535  dn1dc  955  prneimg  3761  f1oprg  5486  fvco4  5568  nnsucuniel  6474  mapen  6824  mapxpen  6826  fidceq  6847  fidifsnen  6848  php5fin  6860  findcard2d  6869  findcard2sd  6870  diffisn  6871  fidcenumlemr  6932  supmoti  6970  djuf1olem  7030  nninfwlpor  7150  exmidfodomrlemim  7178  cc4f  7231  cc4n  7233  subhalfnqq  7376  nqnq0pi  7400  genprndl  7483  genprndu  7484  addlocpr  7498  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  mullocpr  7533  mulnqprlemrl  7535  mulnqprlemru  7536  ltaprlem  7580  aptiprleml  7601  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemladdfu  7639  caucvgprprlemloc  7665  suplocexprlemrl  7679  suplocexprlemru  7681  mulcmpblnrlemg  7702  recexgt0sr  7735  pitonn  7810  rereceu  7851  rimul  8504  receuap  8587  peano5uzti  9320  iooshf  9909  seq3fveq2  10425  seq3id2  10465  seqfeq3  10468  expcl2lemap  10488  mulexpzap  10516  expnlbnd2  10601  hashfacen  10771  absexpzap  11044  fsumf1o  11353  fisum0diag2  11410  fsummulc2  11411  fprodmul  11554  fprodrev  11582  moddvds  11761  dvdsflip  11811  dfgcd3  11965  dfgcd2  11969  lcmgcdlem  12031  cncongr1  12057  hashgcdlem  12192  phisum  12194  pcval  12250  pcqcl  12260  pcid  12277  pcneg  12278  prmpwdvds  12307  pockthg  12309  4sqlem2  12341  setscom  12456  tgcl  12858  epttop  12884  cnpnei  13013  txcn  13069  txdis1cn  13072  imasnopn  13093  hmeoimaf1o  13108  txhmeo  13113  metss2lem  13291  bdxmet  13295  bdmopn  13298  metrest  13300  xmetxp  13301  metcnp  13306  rprelogbmul  13667  logbgcd1irr  13679