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

Theorem e0a 32524
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  32601  3impexpbicomiVD  32613  tratrbVD  32616  idiVD  32619  ancomstVD  32620  ordelordALTVD  32622  equncomiVD  32624  sucidALTVD  32625  sucidVD  32627  ee33VD  32634  undif3VD  32637  onfrALTlem5VD  32640  onfrALTlem4VD  32641  onfrALTlem1VD  32645  onfrALTVD  32646  relopabVD  32656  19.41rgVD  32657  ax6e2ndVD  32663  2sb5ndVD  32665  sb5ALTVD  32668  vk15.4jVD  32669
  Copyright terms: Public domain W3C validator