Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e12 Structured version   Visualization version   GIF version

Theorem e12 39422
Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e12.1 (   𝜑   ▶   𝜓   )
e12.2 (   𝜑   ,   𝜒   ▶   𝜃   )
e12.3 (𝜓 → (𝜃𝜏))
Assertion
Ref Expression
e12 (   𝜑   ,   𝜒   ▶   𝜏   )

Proof of Theorem e12
StepHypRef Expression
1 e12.1 . . 3 (   𝜑   ▶   𝜓   )
21vd12 39296 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 39367 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 39256  (   wvd2 39264
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-an 385  df-vd1 39257  df-vd2 39265
This theorem is referenced by:  e12an  39423  trsspwALT  39516  sspwtr  39519  pwtrVD  39527  snssiALTVD  39530  elex2VD  39541  elex22VD  39542  eqsbc3rVD  39543  en3lplem1VD  39546  3ornot23VD  39550  orbi1rVD  39551  19.21a3con13vVD  39555  exbirVD  39556  tratrbVD  39565  ssralv2VD  39570  sbcim2gVD  39579  sbcbiVD  39580  relopabVD  39605  19.41rgVD  39606  ax6e2eqVD  39611  ax6e2ndeqVD  39613  vk15.4jVD  39618  con3ALTVD  39620
  Copyright terms: Public domain W3C validator