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 40935
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 40811 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 40882 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 40780  (   wvd2 40788
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 208  df-an 397  df-vd1 40781  df-vd2 40789
This theorem is referenced by:  e12an  40936  trsspwALT  41029  sspwtr  41032  pwtrVD  41035  snssiALTVD  41038  elex2VD  41049  elex22VD  41050  eqsbc3rVD  41051  en3lplem1VD  41054  3ornot23VD  41058  orbi1rVD  41059  19.21a3con13vVD  41063  exbirVD  41064  tratrbVD  41072  ssralv2VD  41077  sbcim2gVD  41086  sbcbiVD  41087  relopabVD  41112  19.41rgVD  41113  ax6e2eqVD  41118  ax6e2ndeqVD  41120  vk15.4jVD  41125  con3ALTVD  41127
  Copyright terms: Public domain W3C validator