Theorem e0a 45538

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  45612  3impexpbicomiVD  45624  tratrbVD  45627  idiVD  45630  ancomstVD  45631  ordelordALTVD  45633  equncomiVD  45635  sucidALTVD  45636  sucidVD  45638  ee33VD  45645  undif3VD  45648  onfrALTlem5VD  45651  onfrALTlem1VD  45656  onfrALTVD  45657  relopabVD  45667  19.41rgVD  45668  ax6e2ndVD  45674  2sb5ndVD  45676  sb5ALTVD  45679  vk15.4jVD  45680