Theorem e0a 44763

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  44837  3impexpbicomiVD  44849  tratrbVD  44852  idiVD  44855  ancomstVD  44856  ordelordALTVD  44858  equncomiVD  44860  sucidALTVD  44861  sucidVD  44863  ee33VD  44870  undif3VD  44873  onfrALTlem5VD  44876  onfrALTlem1VD  44881  onfrALTVD  44882  relopabVD  44892  19.41rgVD  44893  ax6e2ndVD  44899  2sb5ndVD  44901  sb5ALTVD  44904  vk15.4jVD  44905