Theorem e0a 38020

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  38103  3impexpbicomiVD  38115  tratrbVD  38119  idiVD  38122  ancomstVD  38123  ordelordALTVD  38125  equncomiVD  38127  sucidALTVD  38128  sucidVD  38130  ee33VD  38137  undif3VD  38140  onfrALTlem5VD  38143  onfrALTlem4VD  38144  onfrALTlem1VD  38148  onfrALTVD  38149  relopabVD  38159  19.41rgVD  38160  ax6e2ndVD  38166  2sb5ndVD  38168  sb5ALTVD  38171  vk15.4jVD  38172