Theorem e0a 45371

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  45445  3impexpbicomiVD  45457  tratrbVD  45460  idiVD  45463  ancomstVD  45464  ordelordALTVD  45466  equncomiVD  45468  sucidALTVD  45469  sucidVD  45471  ee33VD  45478  undif3VD  45481  onfrALTlem5VD  45484  onfrALTlem1VD  45489  onfrALTVD  45490  relopabVD  45500  19.41rgVD  45501  ax6e2ndVD  45507  2sb5ndVD  45509  sb5ALTVD  45512  vk15.4jVD  45513