Theorem e0a 41099

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  41173  3impexpbicomiVD  41185  tratrbVD  41188  idiVD  41191  ancomstVD  41192  ordelordALTVD  41194  equncomiVD  41196  sucidALTVD  41197  sucidVD  41199  ee33VD  41206  undif3VD  41209  onfrALTlem5VD  41212  onfrALTlem1VD  41217  onfrALTVD  41218  relopabVD  41228  19.41rgVD  41229  ax6e2ndVD  41235  2sb5ndVD  41237  sb5ALTVD  41240  vk15.4jVD  41241