Theorem e0a 44812

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  44886  3impexpbicomiVD  44898  tratrbVD  44901  idiVD  44904  ancomstVD  44905  ordelordALTVD  44907  equncomiVD  44909  sucidALTVD  44910  sucidVD  44912  ee33VD  44919  undif3VD  44922  onfrALTlem5VD  44925  onfrALTlem1VD  44930  onfrALTVD  44931  relopabVD  44941  19.41rgVD  44942  ax6e2ndVD  44948  2sb5ndVD  44950  sb5ALTVD  44953  vk15.4jVD  44954