Theorem e0a 45739

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 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  simplbi2VD  45813  3impexpbicomiVD  45825  tratrbVD  45828  idiVD  45831  ancomstVD  45832  ordelordALTVD  45834  equncomiVD  45836  sucidALTVD  45837  sucidVD  45839  ee33VD  45846  undif3VD  45849  onfrALTlem5VD  45852  onfrALTlem1VD  45857  onfrALTVD  45858  relopabVD  45868  19.41rgVD  45869  ax6e2ndVD  45875  2sb5ndVD  45877  sb5ALTVD  45880  vk15.4jVD  45881