Theorem e0a 42281

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  42355  3impexpbicomiVD  42367  tratrbVD  42370  idiVD  42373  ancomstVD  42374  ordelordALTVD  42376  equncomiVD  42378  sucidALTVD  42379  sucidVD  42381  ee33VD  42388  undif3VD  42391  onfrALTlem5VD  42394  onfrALTlem1VD  42399  onfrALTVD  42400  relopabVD  42410  19.41rgVD  42411  ax6e2ndVD  42417  2sb5ndVD  42419  sb5ALTVD  42422  vk15.4jVD  42423