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 39513
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 39416 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 39507 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39379
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 198  df-vd1 39380
This theorem is referenced by:  e10an  39514  en3lpVD  39665  3orbi123VD  39670  sbc3orgVD  39671  exbiriVD  39674  3impexpVD  39676  3impexpbicomVD  39677  al2imVD  39682  equncomVD  39688  trsbcVD  39697  sbcssgVD  39703  csbingVD  39704  onfrALTVD  39711  csbsngVD  39713  csbxpgVD  39714  csbresgVD  39715  csbrngVD  39716  csbima12gALTVD  39717  csbunigVD  39718  csbfv12gALTVD  39719  con5VD  39720  hbimpgVD  39724  hbalgVD  39725  hbexgVD  39726  ax6e2eqVD  39727  ax6e2ndeqVD  39729  e2ebindVD  39732  sb5ALTVD  39733
  Copyright terms: Public domain W3C validator