Theorem e0a 45344

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  45418  3impexpbicomiVD  45430  tratrbVD  45433  idiVD  45436  ancomstVD  45437  ordelordALTVD  45439  equncomiVD  45441  sucidALTVD  45442  sucidVD  45444  ee33VD  45451  undif3VD  45454  onfrALTlem5VD  45457  onfrALTlem1VD  45462  onfrALTVD  45463  relopabVD  45473  19.41rgVD  45474  ax6e2ndVD  45480  2sb5ndVD  45482  sb5ALTVD  45485  vk15.4jVD  45486