Theorem e0a 42392

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  42466  3impexpbicomiVD  42478  tratrbVD  42481  idiVD  42484  ancomstVD  42485  ordelordALTVD  42487  equncomiVD  42489  sucidALTVD  42490  sucidVD  42492  ee33VD  42499  undif3VD  42502  onfrALTlem5VD  42505  onfrALTlem1VD  42510  onfrALTVD  42511  relopabVD  42521  19.41rgVD  42522  ax6e2ndVD  42528  2sb5ndVD  42530  sb5ALTVD  42533  vk15.4jVD  42534