Theorem e00 42277

Description: Elimination rule identical to mp2 9. The non-virtual deduction form is the virtual deduction form, which is mp2 9. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
e00.1	⊢ 𝜑
e00.2	⊢ 𝜓
e00.3	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
e00	⊢ 𝜒

Proof of Theorem e00

Step	Hyp	Ref	Expression
1		e00.1	. 2 ⊢ 𝜑
2		e00.2	. 2 ⊢ 𝜓
3		e00.3	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	mp2 9	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  3impexpVD  42365  3impexpbicomVD  42366