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 41417
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 41293 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 41364 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 41262  (   wvd2 41270
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 210  df-an 400  df-vd1 41263  df-vd2 41271
This theorem is referenced by:  e12an  41418  trsspwALT  41511  sspwtr  41514  pwtrVD  41517  snssiALTVD  41520  elex2VD  41531  elex22VD  41532  eqsbc3rVD  41533  en3lplem1VD  41536  3ornot23VD  41540  orbi1rVD  41541  19.21a3con13vVD  41545  exbirVD  41546  tratrbVD  41554  ssralv2VD  41559  sbcim2gVD  41568  sbcbiVD  41569  relopabVD  41594  19.41rgVD  41595  ax6e2eqVD  41600  ax6e2ndeqVD  41602  vk15.4jVD  41607  con3ALTVD  41609
  Copyright terms: Public domain W3C validator