Theorem e0a 41478

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  41552  3impexpbicomiVD  41564  tratrbVD  41567  idiVD  41570  ancomstVD  41571  ordelordALTVD  41573  equncomiVD  41575  sucidALTVD  41576  sucidVD  41578  ee33VD  41585  undif3VD  41588  onfrALTlem5VD  41591  onfrALTlem1VD  41596  onfrALTVD  41597  relopabVD  41607  19.41rgVD  41608  ax6e2ndVD  41614  2sb5ndVD  41616  sb5ALTVD  41619  vk15.4jVD  41620