Theorem ad2antll 483

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  522  simprrl  529  simprrr  530  dn1dc  950  prneimg  3753  f1oprg  5475  fvco4  5557  nnsucuniel  6459  mapen  6808  mapxpen  6810  fidceq  6831  fidifsnen  6832  php5fin  6844  findcard2d  6853  findcard2sd  6854  diffisn  6855  fidcenumlemr  6916  supmoti  6954  djuf1olem  7014  exmidfodomrlemim  7153  cc4f  7206  cc4n  7208  subhalfnqq  7351  nqnq0pi  7375  genprndl  7458  genprndu  7459  addlocpr  7473  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  mullocpr  7508  mulnqprlemrl  7510  mulnqprlemru  7511  ltaprlem  7555  aptiprleml  7576  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  caucvgprlemladdfu  7614  caucvgprprlemloc  7640  suplocexprlemrl  7654  suplocexprlemru  7656  mulcmpblnrlemg  7677  recexgt0sr  7710  pitonn  7785  rereceu  7826  rimul  8479  receuap  8562  peano5uzti  9295  iooshf  9884  seq3fveq2  10400  seq3id2  10440  seqfeq3  10443  expcl2lemap  10463  mulexpzap  10491  expnlbnd2  10576  hashfacen  10745  absexpzap  11018  fsumf1o  11327  fisum0diag2  11384  fsummulc2  11385  fprodmul  11528  fprodrev  11556  moddvds  11735  dvdsflip  11785  dfgcd3  11939  dfgcd2  11943  lcmgcdlem  12005  cncongr1  12031  hashgcdlem  12166  phisum  12168  pcval  12224  pcqcl  12234  pcid  12251  pcneg  12252  prmpwdvds  12281  pockthg  12283  4sqlem2  12315  setscom  12430  tgcl  12664  epttop  12690  cnpnei  12819  txcn  12875  txdis1cn  12878  imasnopn  12899  hmeoimaf1o  12914  txhmeo  12919  metss2lem  13097  bdxmet  13101  bdmopn  13104  metrest  13106  xmetxp  13107  metcnp  13112  rprelogbmul  13473  logbgcd1irr  13485