Theorem ad2antll 320

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

Ref	Expression
ad2antll	|- (((ph /\ ch) /\ th) -> ps)

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantr 306	. 2 |- ((ph /\ ch) -> ps)
3	2	adantr 306	1 |- (((ph /\ ch) /\ th) -> ps)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  reupick 1578  tz7.7 2224  tz7.49 2997  oaordi 3148  oaass 3163  nnmordi 3188  sbthlem8 3356  onomeneq 3414  unblem1 3431  unblem3 3433  inf3lem5 3468  infensuc 3484  r1ord 3499  ltexpq 3874  genpnnp 3902  addcanpr 3946  prlem936b 3948  suppr 3957  zltp1let 4597  sqr11 4761  sh 5116  occont 5168  chocuni 5179  occllem6 5185  elspansn4t 5478  osumlem6 5535  5oalem1 5544  3oalem2 5553  stelt 5671  atsseq 5745  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org