Theorem ee33VD 45647

Description: Non-virtual deduction form of e33 45502. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ee33 45290 is ee33VD 45647 without virtual deductions and was automatically derived from ee33VD 45647.

h1::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
h2::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
h3::	⊢ (𝜃 → (𝜏 → 𝜂))
4:1,3:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → 𝜂))))
5:4:	⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
6:2,5:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
7:6:	⊢ (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
8:7:	⊢ (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
qed:8:	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
ee33VD	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Proof of Theorem ee33VD

Step	Hyp	Ref	Expression
1		ee33VD.2	. . . . 5 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
2		ee33VD.1	. . . . . . 7 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3		ee33VD.3	. . . . . . 7 ⊢ (𝜃 → (𝜏 → 𝜂))
4	2, 3	syl8 77	. . . . . 6 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → 𝜂))))
5	4	com4r 95	. . . . 5 ⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
6	1, 5	syl8 77	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
7		pm2.43cbi 45287	. . . . 5 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))) ↔ (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
8	7	biimpi 219	. . . 4 ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))) → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
9	6, 8	e0a 45540	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
10		pm2.43cbi 45287	. . . 4 ⊢ ((𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))) ↔ (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
11	10	biimpi 219	. . 3 ⊢ ((𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))) → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
12	9, 11	e0a 45540	. 2 ⊢ (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
13		pm2.43cbi 45287	. . 3 ⊢ ((𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜂))))
14	13	biimpi 219	. 2 ⊢ ((𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))) → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
15	12, 14	e0a 45540	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

This proof depends on syntax axioms:   → wi 4

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

This proof depends on definitions:  df-bi 210

This theorem is used by: (None)