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 44692
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 44595 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 44686 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44567
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 44568
This theorem is referenced by:  e10an  44693  en3lpVD  44843  3orbi123VD  44848  sbc3orgVD  44849  exbiriVD  44852  3impexpVD  44854  3impexpbicomVD  44855  al2imVD  44860  equncomVD  44866  trsbcVD  44875  sbcssgVD  44881  csbingVD  44882  onfrALTVD  44889  csbsngVD  44891  csbxpgVD  44892  csbresgVD  44893  csbrngVD  44894  csbima12gALTVD  44895  csbunigVD  44896  csbfv12gALTVD  44897  con5VD  44898  hbimpgVD  44902  hbalgVD  44903  hbexgVD  44904  ax6e2eqVD  44905  ax6e2ndeqVD  44907  e2ebindVD  44910  sb5ALTVD  44911
  Copyright terms: Public domain W3C validator