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 39316
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  39395  3impexpbicomiVD  39407  tratrbVD  39411  idiVD  39414  ancomstVD  39415  ordelordALTVD  39417  equncomiVD  39419  sucidALTVD  39420  sucidVD  39422  ee33VD  39429  undif3VD  39432  onfrALTlem5VD  39435  onfrALTlem4VD  39436  onfrALTlem1VD  39440  onfrALTVD  39441  relopabVD  39451  19.41rgVD  39452  ax6e2ndVD  39458  2sb5ndVD  39460  sb5ALTVD  39463  vk15.4jVD  39464
  Copyright terms: Public domain W3C validator