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

Theorem e01 28768
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e01.1  |-  ph
e01.2  |-  (. ps  ->.  ch
).
e01.3  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
e01  |-  (. ps  ->.  th
).

Proof of Theorem e01
StepHypRef Expression
1 e01.1 . . 3  |-  ph
21vd01 28674 . 2  |-  (. ps  ->.  ph ).
3 e01.2 . 2  |-  (. ps  ->.  ch
).
4 e01.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4e11 28765 1  |-  (. ps  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636
This theorem is referenced by:  e01an  28770  trsspwALT  28908  sspwtr  28911  pwtrVD  28914  pwtrrVD  28916  snssiALTVD  28918  snelpwrVD  28922  sstrALT2VD  28926  suctrALT2VD  28928  3impexpVD  28948  a9e2eqVD  28999  a9e2ndVD  29000  2sb5ndVD  29002  vk15.4jVD  29006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-vd1 28637
  Copyright terms: Public domain W3C validator