Theorem e0a 45216

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  45290  3impexpbicomiVD  45302  tratrbVD  45305  idiVD  45308  ancomstVD  45309  ordelordALTVD  45311  equncomiVD  45313  sucidALTVD  45314  sucidVD  45316  ee33VD  45323  undif3VD  45326  onfrALTlem5VD  45329  onfrALTlem1VD  45334  onfrALTVD  45335  relopabVD  45345  19.41rgVD  45346  ax6e2ndVD  45352  2sb5ndVD  45354  sb5ALTVD  45357  vk15.4jVD  45358