Theorem e0a 44734

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  44808  3impexpbicomiVD  44820  tratrbVD  44823  idiVD  44826  ancomstVD  44827  ordelordALTVD  44829  equncomiVD  44831  sucidALTVD  44832  sucidVD  44834  ee33VD  44841  undif3VD  44844  onfrALTlem5VD  44847  onfrALTlem1VD  44852  onfrALTVD  44853  relopabVD  44863  19.41rgVD  44864  ax6e2ndVD  44870  2sb5ndVD  44872  sb5ALTVD  44875  vk15.4jVD  44876