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

Theorem e0_ 28884
Description: Elimination rule identical to ax-mp 8. The non-virtual deduction form is the virtual deduction form, which is ax-mp 8. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e0_.1  |-  ph
e0_.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
e0_  |-  ps

Proof of Theorem e0_
StepHypRef Expression
1 e0_.1 . 2  |-  ph
2 e0_.2 . 2  |-  ( ph  ->  ps )
31, 2ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  simplbi2VD  28958  3impexpbicomiVD  28970  tratrbVD  28973  idiVD  28976  ancomsimpVD  28977  ordelordALTVD  28979  equncomiVD  28981  sucidALTVD  28982  sucidVD  28984  ee33VD  28991  undif3VD  28994  onfrALTlem5VD  28997  onfrALTlem4VD  28998  onfrALTlem1VD  29002  onfrALTVD  29003  relopabVD  29013  19.41rgVD  29014  a9e2ndVD  29020  2sb5ndVD  29022  sb5ALTVD  29025  vk15.4jVD  29026
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator