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

Theorem e10 42956
Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e10.1 (   𝜑   ▶   𝜓   )
e10.2 𝜒
e10.3 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
e10 (   𝜑   ▶   𝜃   )

Proof of Theorem e10
StepHypRef Expression
1 e10.1 . 2 (   𝜑   ▶   𝜓   )
2 e10.2 . . 3 𝜒
32vd01 42859 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 42950 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 42831
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 206  df-vd1 42832
This theorem is referenced by:  e10an  42957  en3lpVD  43107  3orbi123VD  43112  sbc3orgVD  43113  exbiriVD  43116  3impexpVD  43118  3impexpbicomVD  43119  al2imVD  43124  equncomVD  43130  trsbcVD  43139  sbcssgVD  43145  csbingVD  43146  onfrALTVD  43153  csbsngVD  43155  csbxpgVD  43156  csbresgVD  43157  csbrngVD  43158  csbima12gALTVD  43159  csbunigVD  43160  csbfv12gALTVD  43161  con5VD  43162  hbimpgVD  43166  hbalgVD  43167  hbexgVD  43168  ax6e2eqVD  43169  ax6e2ndeqVD  43171  e2ebindVD  43174  sb5ALTVD  43175
  Copyright terms: Public domain W3C validator