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 44714
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 44617 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 44708 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44589
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 207  df-vd1 44590
This theorem is referenced by:  e10an  44715  en3lpVD  44865  3orbi123VD  44870  sbc3orgVD  44871  exbiriVD  44874  3impexpVD  44876  3impexpbicomVD  44877  al2imVD  44882  equncomVD  44888  trsbcVD  44897  sbcssgVD  44903  csbingVD  44904  onfrALTVD  44911  csbsngVD  44913  csbxpgVD  44914  csbresgVD  44915  csbrngVD  44916  csbima12gALTVD  44917  csbunigVD  44918  csbfv12gALTVD  44919  con5VD  44920  hbimpgVD  44924  hbalgVD  44925  hbexgVD  44926  ax6e2eqVD  44927  ax6e2ndeqVD  44929  e2ebindVD  44932  sb5ALTVD  44933
  Copyright terms: Public domain W3C validator