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

Theorem e10 28772
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 28674 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28765 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28636
This theorem is referenced by:  e10an  28773  en3lpVD  28937  3orbi123VD  28942  sbc3orgVD  28943  exbiriVD  28946  3impexpVD  28948  3impexpbicomVD  28949  3ax5VD  28954  equncomVD  28960  trsbcVD  28969  sbcssVD  28975  csbingVD  28976  onfrALTVD  28983  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  con5VD  28992  hbimpgVD  28996  hbalgVD  28997  hbexgVD  28998  a9e2eqVD  28999  a9e2ndeqVD  29001  e2ebindVD  29004  sb5ALTVD  29005
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 28637
  Copyright terms: Public domain W3C validator