Theorem e0a 44745

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  44819  3impexpbicomiVD  44831  tratrbVD  44834  idiVD  44837  ancomstVD  44838  ordelordALTVD  44840  equncomiVD  44842  sucidALTVD  44843  sucidVD  44845  ee33VD  44852  undif3VD  44855  onfrALTlem5VD  44858  onfrALTlem1VD  44863  onfrALTVD  44864  relopabVD  44874  19.41rgVD  44875  ax6e2ndVD  44881  2sb5ndVD  44883  sb5ALTVD  44886  vk15.4jVD  44887