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

Theorem e10 36715
Description: A virtual deduction elimination rule (see mpisyl 22). (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 36618 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 36709 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36581
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 188  df-vd1 36582
This theorem is referenced by:  e10an  36716  en3lpVD  36885  3orbi123VD  36890  sbc3orgVD  36891  exbiriVD  36894  3impexpVD  36896  3impexpbicomVD  36897  al2imVD  36903  equncomVD  36909  trsbcVD  36918  sbcssgVD  36924  csbingVD  36925  onfrALTVD  36932  csbsngVD  36934  csbxpgVD  36935  csbresgVD  36936  csbrngVD  36937  csbima12gALTVD  36938  csbunigVD  36939  csbfv12gALTVD  36940  con5VD  36941  hbimpgVD  36945  hbalgVD  36946  hbexgVD  36947  ax6e2eqVD  36948  ax6e2ndeqVD  36950  e2ebindVD  36953  sb5ALTVD  36954
  Copyright terms: Public domain W3C validator