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 44722
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 44598 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 44669 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44567  (   wvd2 44575
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 207  df-an 396  df-vd1 44568  df-vd2 44576
This theorem is referenced by:  e12an  44723  trsspwALT  44816  sspwtr  44819  pwtrVD  44822  snssiALTVD  44825  elex2VD  44836  elex22VD  44837  eqsbc2VD  44838  en3lplem1VD  44841  3ornot23VD  44845  orbi1rVD  44846  19.21a3con13vVD  44850  exbirVD  44851  tratrbVD  44859  ssralv2VD  44864  sbcim2gVD  44873  sbcbiVD  44874  relopabVD  44899  19.41rgVD  44900  ax6e2eqVD  44905  ax6e2ndeqVD  44907  vk15.4jVD  44912  con3ALTVD  44914
  Copyright terms: Public domain W3C validator