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

Theorem e01 28792
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 28698 . 2  |-  (. ps  ->.  ph ).
3 e01.2 . 2  |-  (. ps  ->.  ch
).
4 e01.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4e11 28789 1  |-  (. ps  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28660
This theorem is referenced by:  e01an  28793  trsspwALT  28931  sspwtr  28934  pwtrVD  28937  pwtrrVD  28938  snssiALTVD  28939  snelpwrVD  28943  sstrALT2VD  28946  suctrALT2VD  28948  3impexpVD  28968  a9e2eqVD  29019  a9e2ndVD  29020  2sb5ndVD  29022  vk15.4jVD  29026
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 178  df-vd1 28661
  Copyright terms: Public domain W3C validator