Theorem ee23 1364

Description: e23 in set.mm without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.

Hypotheses

Ref	Expression
ee23.1	|- (ph -> (ps -> ch))
ee23.2	|- (ph -> (ps -> (th -> ta)))
ee23.3	|- (ch -> (ta -> et))

Assertion

Ref	Expression
ee23	|- (ph -> (ps -> (th -> et)))

Proof of Theorem ee23

Step	Hyp	Ref	Expression
1		ee23.2	. 2 |- (ph -> (ps -> (th -> ta)))
2		ee23.1	. . 3 |- (ph -> (ps -> ch))
3		ee23.3	. . 3 |- (ch -> (ta -> et))
4	2, 3	syl6 29	. 2 |- (ph -> (ps -> (ta -> et)))
5	1, 4	syldd 61	1 |- (ph -> (ps -> (th -> et)))

Syntax hints:   -> wi 4

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

This theorem is referenced by: (None)