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

Assertion

Ref	Expression
ee23	⊢ (φ → (ψ → (θ → η)))

Proof of Theorem ee23

Step	Hyp	Ref	Expression
1		ee23.2	. 2 ⊢ (φ → (ψ → (θ → τ)))
2		ee23.1	. . 3 ⊢ (φ → (ψ → χ))
3		ee23.3	. . 3 ⊢ (χ → (τ → η))
4	2, 3	syl6 29	. 2 ⊢ (φ → (ψ → (τ → η)))
5	1, 4	syldd 61	1 ⊢ (φ → (ψ → (θ → η)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by: (None)