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

Theorem e0_ 28547
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  28622  3impexpbicomiVD  28634  tratrbVD  28637  idiVD  28640  ancomsimpVD  28641  ordelordALTVD  28643  equncomiVD  28645  sucidALTVD  28646  sucidVD  28648  ee33VD  28655  undif3VD  28658  onfrALTlem5VD  28661  onfrALTlem4VD  28662  onfrALTlem1VD  28666  onfrALTVD  28667  relopabVD  28677  19.41rgVD  28678  a9e2ndVD  28684  2sb5ndVD  28686  sb5ALTVD  28689  vk15.4jVD  28690
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator