Theorem e0a 43837

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  43911  3impexpbicomiVD  43923  tratrbVD  43926  idiVD  43929  ancomstVD  43930  ordelordALTVD  43932  equncomiVD  43934  sucidALTVD  43935  sucidVD  43937  ee33VD  43944  undif3VD  43947  onfrALTlem5VD  43950  onfrALTlem1VD  43955  onfrALTVD  43956  relopabVD  43966  19.41rgVD  43967  ax6e2ndVD  43973  2sb5ndVD  43975  sb5ALTVD  43978  vk15.4jVD  43979