Theorem e000

Description: A virtual deduction elimination rule. The non-virtual deduction form of e000 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	e000.1	⊢ 𝜑
	e000.2	⊢ 𝜓
	e000.3	⊢ 𝜒
	e000.4	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
Assertion	e000	⊢ 𝜃

Proof

Step	Hyp	Ref	Expression
1		e000.1	⊢ 𝜑
2		e000.2	⊢ 𝜓
3		e000.3	⊢ 𝜒
4		e000.4	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
5	1 2 4	mp2	⊢ ( 𝜒 → 𝜃 )
6	3 5	ax-mp	⊢ 𝜃