Theorem e0a 45862

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  45936  3impexpbicomiVD  45948  tratrbVD  45951  idiVD  45954  ancomstVD  45955  ordelordALTVD  45957  equncomiVD  45959  sucidALTVD  45960  sucidVD  45962  ee33VD  45969  undif3VD  45972  onfrALTlem5VD  45975  onfrALTlem1VD  45980  onfrALTVD  45981  relopabVD  45991  19.41rgVD  45992  ax6e2ndVD  45998  2sb5ndVD  46000  sb5ALTVD  46003  vk15.4jVD  46004