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

Theorem e10 28208
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 28110 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 28201 1  |-  (. ph  ->.  th
).
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28072
This theorem is referenced by:  e10an  28209  en3lpVD  28373  3orbi123VD  28378  sbc3orgVD  28379  exbiriVD  28382  3impexpVD  28384  3impexpbicomVD  28385  3ax5VD  28390  equncomVD  28396  trsbcVD  28405  sbcssVD  28411  csbingVD  28412  onfrALTVD  28419  csbsngVD  28421  csbxpgVD  28422  csbresgVD  28423  csbrngVD  28424  csbima12gALTVD  28425  csbunigVD  28426  csbfv12gALTVD  28427  con5VD  28428  hbimpgVD  28432  hbalgVD  28433  hbexgVD  28434  a9e2eqVD  28435  a9e2ndeqVD  28437  e2ebindVD  28440  sb5ALTVD  28441
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 28073
  Copyright terms: Public domain W3C validator