Theorem e333

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		e333.1	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
2		e333.2	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜏    )
3		e333.3	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜂    )
4		e333.4	⊢ ( 𝜃 → ( 𝜏 → ( 𝜂 → 𝜁 ) ) )
5	3	dfvd3i	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜂 ) ) )
6	5	3imp	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜂 )
7	1	dfvd3i	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
8	7	3imp	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
9	2	dfvd3i	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜏 ) ) )
10	9	3imp	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜏 )
11	8 10 4	syl2im	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜂 → 𝜁 ) ) )
12	11	pm2.43i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜂 → 𝜁 ) )
13	6 12	syl5com	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜁 ) )
14	13	pm2.43i	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜁 )
15	14	3exp	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜁 ) ) )
16	15	dfvd3ir	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜁    )