Theorem e0a 44954

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  45028  3impexpbicomiVD  45040  tratrbVD  45043  idiVD  45046  ancomstVD  45047  ordelordALTVD  45049  equncomiVD  45051  sucidALTVD  45052  sucidVD  45054  ee33VD  45061  undif3VD  45064  onfrALTlem5VD  45067  onfrALTlem1VD  45072  onfrALTVD  45073  relopabVD  45083  19.41rgVD  45084  ax6e2ndVD  45090  2sb5ndVD  45092  sb5ALTVD  45095  vk15.4jVD  45096