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

Theorem e10 33666
Description: A virtual deduction elimination rule (see mpisyl 18). (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 33569 . 2  |-  (. ph  ->.  ch
).
4 e10.3 . 2  |-  ( ps 
->  ( ch  ->  th )
)
51, 3, 4e11 33660 1  |-  (. ph  ->.  th
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33532
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 185  df-vd1 33533
This theorem is referenced by:  e10an  33667  en3lpVD  33831  3orbi123VD  33836  sbc3orgVD  33837  exbiriVD  33840  3impexpVD  33842  3impexpbicomVD  33843  al2imVD  33848  equncomVD  33854  trsbcVD  33863  sbcssgVD  33869  csbingVD  33870  onfrALTVD  33877  csbsngVD  33879  csbxpgVD  33880  csbresgVD  33881  csbrngVD  33882  csbima12gALTVD  33883  csbunigVD  33884  csbfv12gALTVD  33885  con5VD  33886  hbimpgVD  33890  hbalgVD  33891  hbexgVD  33892  ax6e2eqVD  33893  ax6e2ndeqVD  33895  e2ebindVD  33898  sb5ALTVD  33899
  Copyright terms: Public domain W3C validator