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

Theorem e0a 36593
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  |-  ph
e0a.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
e0a  |-  ps

Proof of Theorem e0a
StepHypRef Expression
1 e0a.1 . 2  |-  ph
2 e0a.2 . 2  |-  ( ph  ->  ps )
31, 2ax-mp 5 1  |-  ps
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  36676  3impexpbicomiVD  36688  tratrbVD  36692  idiVD  36695  ancomstVD  36696  ordelordALTVD  36698  equncomiVD  36700  sucidALTVD  36701  sucidVD  36703  ee33VD  36710  undif3VD  36713  onfrALTlem5VD  36716  onfrALTlem4VD  36717  onfrALTlem1VD  36721  onfrALTVD  36722  relopabVD  36732  19.41rgVD  36733  ax6e2ndVD  36739  2sb5ndVD  36741  sb5ALTVD  36744  vk15.4jVD  36745
  Copyright terms: Public domain W3C validator