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

Theorem e10 28893
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 28796 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28887 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28758
This theorem is referenced by:  e10an  28894  en3lpVD  29055  3orbi123VD  29060  sbc3orgVD  29061  exbiriVD  29064  3impexpVD  29066  3impexpbicomVD  29067  3ax5VD  29072  equncomVD  29078  trsbcVD  29087  sbcssVD  29093  csbingVD  29094  onfrALTVD  29101  csbsngVD  29103  csbxpgVD  29104  csbresgVD  29105  csbrngVD  29106  csbima12gALTVD  29107  csbunigVD  29108  csbfv12gALTVD  29109  con5VD  29110  hbimpgVD  29114  hbalgVD  29115  hbexgVD  29116  a9e2eqVD  29117  a9e2ndeqVD  29119  e2ebindVD  29122  sb5ALTVD  29123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-vd1 28759
  Copyright terms: Public domain W3C validator