Theorem syldd 61

Description: Nested syllogism deduction. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 11-May-2013.)

Hypotheses

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

Assertion

Ref	Expression
syldd	|- (ph -> (ps -> (ch -> ta)))

Proof of Theorem syldd

Step	Hyp	Ref	Expression
1		syldd.2	. 2 |- (ph -> (ps -> (th -> ta)))
2		syldd.1	. 2 |- (ph -> (ps -> (ch -> th)))
3		imim2 49	. 2 |- ((th -> ta) -> ((ch -> th) -> (ch -> ta)))
4	1, 2, 3	syl6c 60	1 |- (ph -> (ps -> (ch -> ta)))

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl5d  62  syl6d  64  ee23  1364