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

Theorem e01 28463
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 28369 . 2  |-  (. ps  ->.  ph ).
3 e01.2 . 2  |-  (. ps  ->.  ch
).
4 e01.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4e11 28460 1  |-  (. ps  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337
This theorem is referenced by:  e01an  28465  trsspwALT  28592  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  snssiALTVD  28602  snelpwrVD  28606  sstrALT2VD  28610  suctrALT2VD  28612  3impexpVD  28632  a9e2eqVD  28683  a9e2ndVD  28684  2sb5ndVD  28686  vk15.4jVD  28690
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 28338
  Copyright terms: Public domain W3C validator