Theorem e323

Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		e323.1	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
2		e323.2	⊢ (    𝜑    ,    𝜓    ▶    𝜏    )
3		e323.3	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜂    )
4		e323.4	⊢ ( 𝜃 → ( 𝜏 → ( 𝜂 → 𝜁 ) ) )
5	1	dfvd3i	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
6	2	dfvd2i	⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) )
7	3	dfvd3i	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜂 ) ) )
8	5 6 7 4	ee323	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜁 ) ) )
9	8	dfvd3ir	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜁    )