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

Theorem e10 28467
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 28369 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28460 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337
This theorem is referenced by:  e10an  28468  en3lpVD  28621  3orbi123VD  28626  sbc3orgVD  28627  exbiriVD  28630  3impexpVD  28632  3impexpbicomVD  28633  3ax5VD  28638  equncomVD  28644  trsbcVD  28653  sbcssVD  28659  csbingVD  28660  onfrALTVD  28667  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  con5VD  28676  hbimpgVD  28680  hbalgVD  28681  hbexgVD  28682  a9e2eqVD  28683  a9e2ndeqVD  28685  e2ebindVD  28688  sb5ALTVD  28689
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