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	⊢ (φ → (ψ → χ))
ee22.2	⊢ (φ → (ψ → θ))
ee22.3	⊢ (χ → (θ → τ))

Assertion

Ref	Expression
ee22	⊢ (φ → (ψ → τ))

Proof of Theorem ee22

Step	Hyp	Ref	Expression
1		ee22.1	. 2 ⊢ (φ → (ψ → χ))
2		ee22.2	. 2 ⊢ (φ → (ψ → θ))
3		ee22.3	. 2 ⊢ (χ → (θ → τ))
4	1, 2, 3	syl6c 60	1 ⊢ (φ → (ψ → τ))

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  4599