Theorem e0a 38999

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

Hypotheses

Ref	Expression
e0a.1	⊢ 𝜑
e0a.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
e0a	⊢ 𝜓

Proof of Theorem e0a

Step	Hyp	Ref	Expression
1		e0a.1	. 2 ⊢ 𝜑
2		e0a.2	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  simplbi2VD  39081  3impexpbicomiVD  39093  tratrbVD  39097  idiVD  39100  ancomstVD  39101  ordelordALTVD  39103  equncomiVD  39105  sucidALTVD  39106  sucidVD  39108  ee33VD  39115  undif3VD  39118  onfrALTlem5VD  39121  onfrALTlem4VD  39122  onfrALTlem1VD  39126  onfrALTVD  39127  relopabVD  39137  19.41rgVD  39138  ax6e2ndVD  39144  2sb5ndVD  39146  sb5ALTVD  39149  vk15.4jVD  39150