Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e0a Structured version   Visualization version   GIF version

Theorem e0a 44797
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
StepHypRef Expression
1 e0a.1 . 2 𝜑
2 e0a.2 . 2 (𝜑𝜓)
31, 2ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  simplbi2VD  44871  3impexpbicomiVD  44883  tratrbVD  44886  idiVD  44889  ancomstVD  44890  ordelordALTVD  44892  equncomiVD  44894  sucidALTVD  44895  sucidVD  44897  ee33VD  44904  undif3VD  44907  onfrALTlem5VD  44910  onfrALTlem1VD  44915  onfrALTVD  44916  relopabVD  44926  19.41rgVD  44927  ax6e2ndVD  44933  2sb5ndVD  44935  sb5ALTVD  44938  vk15.4jVD  44939
  Copyright terms: Public domain W3C validator