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

Theorem e10 28504
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 28407 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28498 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28369
This theorem is referenced by:  e10an  28505  en3lpVD  28666  3orbi123VD  28671  sbc3orgVD  28672  exbiriVD  28675  3impexpVD  28677  3impexpbicomVD  28678  3ax5VD  28683  equncomVD  28689  trsbcVD  28698  sbcssVD  28704  csbingVD  28705  onfrALTVD  28712  csbsngVD  28714  csbxpgVD  28715  csbresgVD  28716  csbrngVD  28717  csbima12gALTVD  28718  csbunigVD  28719  csbfv12gALTVD  28720  con5VD  28721  hbimpgVD  28725  hbalgVD  28726  hbexgVD  28727  a9e2eqVD  28728  a9e2ndeqVD  28730  e2ebindVD  28733  sb5ALTVD  28734
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 28370
  Copyright terms: Public domain W3C validator