Theorem syl34d 29

Description: Deduction combining antecedents and consequents.

Hypotheses

Ref	Expression
syl34d.1	|- (ph -> (ps -> ch))
syl34d.2	|- (ph -> (th -> ta ))

Assertion

Ref	Expression
syl34d	|- (ph -> ((ch -> th) -> (ps -> ta )))

Proof of Theorem syl34d

Step	Hyp	Ref	Expression
1		syl34d.1	. . 3 |- (ph -> (ps -> ch))
2	1	syl4d 28	. 2 |- (ph -> ((ch -> th) -> (ps -> th)))
3		syl34d.2	. . 3 |- (ph -> (th -> ta ))
4	3	syl3d 26	. 2 |- (ph -> ((ps -> th) -> (ps -> ta )))
5	2, 4	syld 27	1 |- (ph -> ((ch -> th) -> (ps -> ta )))

Syntax hints:   -> wi 2

This theorem is referenced by:  pm3.48 430  mo 1020  peano5 2394  tfrlem1 2949  uzind 4603  dmdbr 5731

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

metamath.org