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 38739
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 38642 . 2 (   𝜑   ▶   𝜒   )
4 e10.3 . 2 (𝜓 → (𝜒𝜃))
51, 3, 4e11 38733 1 (   𝜑   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 38605
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 38606
This theorem is referenced by:  e10an  38740  en3lpVD  38900  3orbi123VD  38905  sbc3orgVD  38906  exbiriVD  38909  3impexpVD  38911  3impexpbicomVD  38912  al2imVD  38918  equncomVD  38924  trsbcVD  38933  sbcssgVD  38939  csbingVD  38940  onfrALTVD  38947  csbsngVD  38949  csbxpgVD  38950  csbresgVD  38951  csbrngVD  38952  csbima12gALTVD  38953  csbunigVD  38954  csbfv12gALTVD  38955  con5VD  38956  hbimpgVD  38960  hbalgVD  38961  hbexgVD  38962  ax6e2eqVD  38963  ax6e2ndeqVD  38965  e2ebindVD  38968  sb5ALTVD  38969
  Copyright terms: Public domain W3C validator