Theorem e0a 44743

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  44817  3impexpbicomiVD  44829  tratrbVD  44832  idiVD  44835  ancomstVD  44836  ordelordALTVD  44838  equncomiVD  44840  sucidALTVD  44841  sucidVD  44843  ee33VD  44850  undif3VD  44853  onfrALTlem5VD  44856  onfrALTlem1VD  44861  onfrALTVD  44862  relopabVD  44872  19.41rgVD  44873  ax6e2ndVD  44879  2sb5ndVD  44881  sb5ALTVD  44884  vk15.4jVD  44885