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 39236
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 39139 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 39230 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39102
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 197  df-vd1 39103
This theorem is referenced by:  e10an  39237  en3lpVD  39394  3orbi123VD  39399  sbc3orgVD  39400  exbiriVD  39403  3impexpVD  39405  3impexpbicomVD  39406  al2imVD  39412  equncomVD  39418  trsbcVD  39427  sbcssgVD  39433  csbingVD  39434  onfrALTVD  39441  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  hbimpgVD  39454  hbalgVD  39455  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndeqVD  39459  e2ebindVD  39462  sb5ALTVD  39463
  Copyright terms: Public domain W3C validator