Theorem e0a 45127

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  45201  3impexpbicomiVD  45213  tratrbVD  45216  idiVD  45219  ancomstVD  45220  ordelordALTVD  45222  equncomiVD  45224  sucidALTVD  45225  sucidVD  45227  ee33VD  45234  undif3VD  45237  onfrALTlem5VD  45240  onfrALTlem1VD  45245  onfrALTVD  45246  relopabVD  45256  19.41rgVD  45257  ax6e2ndVD  45263  2sb5ndVD  45265  sb5ALTVD  45268  vk15.4jVD  45269