Theorem e0a 43466

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  43540  3impexpbicomiVD  43552  tratrbVD  43555  idiVD  43558  ancomstVD  43559  ordelordALTVD  43561  equncomiVD  43563  sucidALTVD  43564  sucidVD  43566  ee33VD  43573  undif3VD  43576  onfrALTlem5VD  43579  onfrALTlem1VD  43584  onfrALTVD  43585  relopabVD  43595  19.41rgVD  43596  ax6e2ndVD  43602  2sb5ndVD  43604  sb5ALTVD  43607  vk15.4jVD  43608