Theorem e0a 45215

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  45289  3impexpbicomiVD  45301  tratrbVD  45304  idiVD  45307  ancomstVD  45308  ordelordALTVD  45310  equncomiVD  45312  sucidALTVD  45313  sucidVD  45315  ee33VD  45322  undif3VD  45325  onfrALTlem5VD  45328  onfrALTlem1VD  45333  onfrALTVD  45334  relopabVD  45344  19.41rgVD  45345  ax6e2ndVD  45351  2sb5ndVD  45353  sb5ALTVD  45356  vk15.4jVD  45357