Theorem ee22 1362

Description: Virtual deduction rule e22 in set.mm without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 2-May-2011.) (New usage is discouraged.) TODO: decide if this is worth keeping.

Hypotheses

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

Assertion

Ref	Expression
ee22	|- (ph -> (ps -> ta))

Proof of Theorem ee22

Step	Hyp	Ref	Expression
1		ee22.1	. 2 |- (ph -> (ps -> ch))
2		ee22.2	. 2 |- (ph -> (ps -> th))
3		ee22.3	. 2 |- (ch -> (th -> ta))
4	1, 2, 3	syl6c 60	1 |- (ph -> (ps -> 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:  ee21  1375  phi011lem1  4598