Theorem e0a 46014

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 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  simplbi2VD  46088  3impexpbicomiVD  46100  tratrbVD  46103  idiVD  46106  ancomstVD  46107  ordelordALTVD  46109  equncomiVD  46111  sucidALTVD  46112  sucidVD  46114  ee33VD  46121  undif3VD  46124  onfrALTlem5VD  46127  onfrALTlem1VD  46132  onfrALTVD  46133  relopabVD  46143  19.41rgVD  46144  ax6e2ndVD  46150  2sb5ndVD  46152  sb5ALTVD  46155  vk15.4jVD  46156