Theorem ee223

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

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

Proof

Step	Hyp	Ref	Expression
1		ee223.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		ee223.2	⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
3		ee223.3	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜂 ) ) )
4		ee223.4	⊢ ( 𝜒 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) )
5	1 4	syl6	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) ) )
6	5	com34	⊢ ( 𝜑 → ( 𝜓 → ( 𝜂 → ( 𝜃 → 𝜁 ) ) ) )
7	6	com23	⊢ ( 𝜑 → ( 𝜂 → ( 𝜓 → ( 𝜃 → 𝜁 ) ) ) )
8	7	com12	⊢ ( 𝜂 → ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜁 ) ) ) )
9	3 8	syl8	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜁 ) ) ) ) ) )
10	9	com34	⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 → ( 𝜏 → ( 𝜓 → ( 𝜃 → 𝜁 ) ) ) ) ) )
11	10	pm2.43a	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → ( 𝜓 → ( 𝜃 → 𝜁 ) ) ) ) )
12	11	com34	⊢ ( 𝜑 → ( 𝜓 → ( 𝜓 → ( 𝜏 → ( 𝜃 → 𝜁 ) ) ) ) )
13	12	pm2.43d	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → ( 𝜃 → 𝜁 ) ) ) )
14	13	com34	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → ( 𝜏 → 𝜁 ) ) ) )
15	2 14	mpdd	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜁 ) ) )