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 44749
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 44625 . 2 (   𝜑   ,   𝜒   ▶   𝜓   )
3 e12.2 . 2 (   𝜑   ,   𝜒   ▶   𝜃   )
4 e12.3 . 2 (𝜓 → (𝜃𝜏))
52, 3, 4e22 44696 1 (   𝜑   ,   𝜒   ▶   𝜏   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd1 44594  (   wvd2 44602
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 44595  df-vd2 44603
This theorem is referenced by:  e12an  44750  trsspwALT  44843  sspwtr  44846  pwtrVD  44849  snssiALTVD  44852  elex2VD  44863  elex22VD  44864  eqsbc2VD  44865  en3lplem1VD  44868  3ornot23VD  44872  orbi1rVD  44873  19.21a3con13vVD  44877  exbirVD  44878  tratrbVD  44886  ssralv2VD  44891  sbcim2gVD  44900  sbcbiVD  44901  relopabVD  44926  19.41rgVD  44927  ax6e2eqVD  44932  ax6e2ndeqVD  44934  vk15.4jVD  44939  con3ALTVD  44941
  Copyright terms: Public domain W3C validator