Theorem e0a 42631

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  42705  3impexpbicomiVD  42717  tratrbVD  42720  idiVD  42723  ancomstVD  42724  ordelordALTVD  42726  equncomiVD  42728  sucidALTVD  42729  sucidVD  42731  ee33VD  42738  undif3VD  42741  onfrALTlem5VD  42744  onfrALTlem1VD  42749  onfrALTVD  42750  relopabVD  42760  19.41rgVD  42761  ax6e2ndVD  42767  2sb5ndVD  42769  sb5ALTVD  42772  vk15.4jVD  42773