Theorem ee223 42207

Description: e223 42208 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ee223.1	⊢ (𝜑 → (𝜓 → 𝜒))
ee223.2	⊢ (𝜑 → (𝜓 → 𝜃))
ee223.3	⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))
ee223.4	⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))

Assertion

Ref	Expression
ee223	⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁)))

Proof of Theorem ee223

Step	Hyp	Ref	Expression
1		ee223.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
2		ee223.3	. . . . . . . 8 ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))
3		ee223.1	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝜓 → 𝜒))
4		ee223.4	. . . . . . . . . . . 12 ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))
5	3, 4	syl6 35	. . . . . . . . . . 11 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜂 → 𝜁))))
6	5	com34 91	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → (𝜂 → (𝜃 → 𝜁))))
7	6	com23 86	. . . . . . . . 9 ⊢ (𝜑 → (𝜂 → (𝜓 → (𝜃 → 𝜁))))
8	7	com12 32	. . . . . . . 8 ⊢ (𝜂 → (𝜑 → (𝜓 → (𝜃 → 𝜁))))
9	2, 8	syl8 76	. . . . . . 7 ⊢ (𝜑 → (𝜓 → (𝜏 → (𝜑 → (𝜓 → (𝜃 → 𝜁))))))
10	9	com34 91	. . . . . 6 ⊢ (𝜑 → (𝜓 → (𝜑 → (𝜏 → (𝜓 → (𝜃 → 𝜁))))))
11	10	pm2.43a 54	. . . . 5 ⊢ (𝜑 → (𝜓 → (𝜏 → (𝜓 → (𝜃 → 𝜁)))))
12	11	com34 91	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜓 → (𝜏 → (𝜃 → 𝜁)))))
13	12	pm2.43d 53	. . 3 ⊢ (𝜑 → (𝜓 → (𝜏 → (𝜃 → 𝜁))))
14	13	com34 91	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜏 → 𝜁))))
15	1, 14	mpdd 43	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:  e223  42208