Theorem e0a 45480

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  45554  3impexpbicomiVD  45566  tratrbVD  45569  idiVD  45572  ancomstVD  45573  ordelordALTVD  45575  equncomiVD  45577  sucidALTVD  45578  sucidVD  45580  ee33VD  45587  undif3VD  45590  onfrALTlem5VD  45593  onfrALTlem1VD  45598  onfrALTVD  45599  relopabVD  45609  19.41rgVD  45610  ax6e2ndVD  45616  2sb5ndVD  45618  sb5ALTVD  45621  vk15.4jVD  45622