Theorem e0a 44761

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  44835  3impexpbicomiVD  44847  tratrbVD  44850  idiVD  44853  ancomstVD  44854  ordelordALTVD  44856  equncomiVD  44858  sucidALTVD  44859  sucidVD  44861  ee33VD  44868  undif3VD  44871  onfrALTlem5VD  44874  onfrALTlem1VD  44879  onfrALTVD  44880  relopabVD  44890  19.41rgVD  44891  ax6e2ndVD  44897  2sb5ndVD  44899  sb5ALTVD  44902  vk15.4jVD  44903