Theorem e0a 45012

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  45086  3impexpbicomiVD  45098  tratrbVD  45101  idiVD  45104  ancomstVD  45105  ordelordALTVD  45107  equncomiVD  45109  sucidALTVD  45110  sucidVD  45112  ee33VD  45119  undif3VD  45122  onfrALTlem5VD  45125  onfrALTlem1VD  45130  onfrALTVD  45131  relopabVD  45141  19.41rgVD  45142  ax6e2ndVD  45148  2sb5ndVD  45150  sb5ALTVD  45153  vk15.4jVD  45154