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

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

Proof of Theorem e10
StepHypRef Expression
1 e10.1 . 2  |-  (. ph  ->.  ps
).
2 e10.2 . . 3  |-  ch
32vd01 28760 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28851 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28722
This theorem is referenced by:  e10an  28858  en3lpVD  29019  3orbi123VD  29024  sbc3orgVD  29025  exbiriVD  29028  3impexpVD  29030  3impexpbicomVD  29031  3ax5VD  29036  equncomVD  29042  trsbcVD  29051  sbcssVD  29057  csbingVD  29058  onfrALTVD  29065  csbsngVD  29067  csbxpgVD  29068  csbresgVD  29069  csbrngVD  29070  csbima12gALTVD  29071  csbunigVD  29072  csbfv12gALTVD  29073  con5VD  29074  hbimpgVD  29078  hbalgVD  29079  hbexgVD  29080  a9e2eqVD  29081  a9e2ndeqVD  29083  e2ebindVD  29086  sb5ALTVD  29087
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 179  df-vd1 28723
  Copyright terms: Public domain W3C validator