Theorem e123

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

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

Proof

Step	Hyp	Ref	Expression
1		e123.1	⊢ (    𝜑    ▶    𝜓    )
2		e123.2	⊢ (    𝜑    ,    𝜒    ▶    𝜃    )
3		e123.3	⊢ (    𝜑    ,    𝜒    ,    𝜏    ▶    𝜂    )
4		e123.4	⊢ ( 𝜓 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) )
5	1	vd13	⊢ (    𝜑    ,    𝜒    ,    𝜏    ▶    𝜓    )
6	2	vd23	⊢ (    𝜑    ,    𝜒    ,    𝜏    ▶    𝜃    )
7	5 6 3 4	e333	⊢ (    𝜑    ,    𝜒    ,    𝜏    ▶    𝜁    )