Theorem e0a 41126

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  41200  3impexpbicomiVD  41212  tratrbVD  41215  idiVD  41218  ancomstVD  41219  ordelordALTVD  41221  equncomiVD  41223  sucidALTVD  41224  sucidVD  41226  ee33VD  41233  undif3VD  41236  onfrALTlem5VD  41239  onfrALTlem1VD  41244  onfrALTVD  41245  relopabVD  41255  19.41rgVD  41256  ax6e2ndVD  41262  2sb5ndVD  41264  sb5ALTVD  41267  vk15.4jVD  41268