Theorem e0a 45219

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  45293  3impexpbicomiVD  45305  tratrbVD  45308  idiVD  45311  ancomstVD  45312  ordelordALTVD  45314  equncomiVD  45316  sucidALTVD  45317  sucidVD  45319  ee33VD  45326  undif3VD  45329  onfrALTlem5VD  45332  onfrALTlem1VD  45337  onfrALTVD  45338  relopabVD  45348  19.41rgVD  45349  ax6e2ndVD  45355  2sb5ndVD  45357  sb5ALTVD  45360  vk15.4jVD  45361