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 41348
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 41251 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 41342 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 41223
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 210  df-vd1 41224
This theorem is referenced by:  e10an  41349  en3lpVD  41499  3orbi123VD  41504  sbc3orgVD  41505  exbiriVD  41508  3impexpVD  41510  3impexpbicomVD  41511  al2imVD  41516  equncomVD  41522  trsbcVD  41531  sbcssgVD  41537  csbingVD  41538  onfrALTVD  41545  csbsngVD  41547  csbxpgVD  41548  csbresgVD  41549  csbrngVD  41550  csbima12gALTVD  41551  csbunigVD  41552  csbfv12gALTVD  41553  con5VD  41554  hbimpgVD  41558  hbalgVD  41559  hbexgVD  41560  ax6e2eqVD  41561  ax6e2ndeqVD  41563  e2ebindVD  41566  sb5ALTVD  41567
  Copyright terms: Public domain W3C validator