Theorem e0a 45594

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  45668  3impexpbicomiVD  45680  tratrbVD  45683  idiVD  45686  ancomstVD  45687  ordelordALTVD  45689  equncomiVD  45691  sucidALTVD  45692  sucidVD  45694  ee33VD  45701  undif3VD  45704  onfrALTlem5VD  45707  onfrALTlem1VD  45712  onfrALTVD  45713  relopabVD  45723  19.41rgVD  45724  ax6e2ndVD  45730  2sb5ndVD  45732  sb5ALTVD  45735  vk15.4jVD  45736