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 40515
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 40391 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 40462 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 40360  (   wvd2 40368
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 199  df-an 388  df-vd1 40361  df-vd2 40369
This theorem is referenced by:  e12an  40516  trsspwALT  40609  sspwtr  40612  pwtrVD  40615  snssiALTVD  40618  elex2VD  40629  elex22VD  40630  eqsbc3rVD  40631  en3lplem1VD  40634  3ornot23VD  40638  orbi1rVD  40639  19.21a3con13vVD  40643  exbirVD  40644  tratrbVD  40652  ssralv2VD  40657  sbcim2gVD  40666  sbcbiVD  40667  relopabVD  40692  19.41rgVD  40693  ax6e2eqVD  40698  ax6e2ndeqVD  40700  vk15.4jVD  40705  con3ALTVD  40707
  Copyright terms: Public domain W3C validator