This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜁 ) ) )