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

Theorem e0_ 28861
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  28938  3impexpbicomiVD  28950  tratrbVD  28953  idiVD  28956  ancomsimpVD  28957  ordelordALTVD  28959  equncomiVD  28961  sucidALTVD  28962  sucidVD  28964  ee33VD  28971  undif3VD  28974  onfrALTlem5VD  28977  onfrALTlem4VD  28978  onfrALTlem1VD  28982  onfrALTVD  28983  relopabVD  28993  19.41rgVD  28994  a9e2ndVD  29000  2sb5ndVD  29002  sb5ALTVD  29005  vk15.4jVD  29006
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator