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

Theorem e0a 31808
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  31885  3impexpbicomiVD  31897  tratrbVD  31900  idiVD  31903  ancomstVD  31904  ordelordALTVD  31906  equncomiVD  31908  sucidALTVD  31909  sucidVD  31911  ee33VD  31918  undif3VD  31921  onfrALTlem5VD  31924  onfrALTlem4VD  31925  onfrALTlem1VD  31929  onfrALTVD  31930  relopabVD  31940  19.41rgVD  31941  ax6e2ndVD  31947  2sb5ndVD  31949  sb5ALTVD  31952  vk15.4jVD  31953
  Copyright terms: Public domain W3C validator