Theorem syldd 50

Description: Nested syllogism deduction.

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.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		syldd.2	. . 3 |- (ph -> (ps -> (th -> ta)))
3		imim2 14	. . 3 |- ((th -> ta) -> ((ch -> th) -> (ch -> ta)))
4	2, 3	syl6 22	. 2 |- (ph -> (ps -> ((ch -> th) -> (ch -> ta))))
5	1, 4	mpdd 46	1 |- (ph -> (ps -> (ch -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl5d 55  syl6d 56  tz7.49 3959  prlem934 5139  climaddlem3 7116  climmullem8 7127

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

Copyright terms: Public domain