Theorem e0a 45198

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  45272  3impexpbicomiVD  45284  tratrbVD  45287  idiVD  45290  ancomstVD  45291  ordelordALTVD  45293  equncomiVD  45295  sucidALTVD  45296  sucidVD  45298  ee33VD  45305  undif3VD  45308  onfrALTlem5VD  45311  onfrALTlem1VD  45316  onfrALTVD  45317  relopabVD  45327  19.41rgVD  45328  ax6e2ndVD  45334  2sb5ndVD  45336  sb5ALTVD  45339  vk15.4jVD  45340