Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e2 Structured version   Visualization version   GIF version

Theorem e2 44629
Description: A virtual deduction elimination rule. syl6 35 is e2 44629 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e2.1 (   𝜑   ,   𝜓   ▶   𝜒   )
e2.2 (𝜒𝜃)
Assertion
Ref Expression
e2 (   𝜑   ,   𝜓   ▶   𝜃   )

Proof of Theorem e2
StepHypRef Expression
1 e2.1 . . . 4 (   𝜑   ,   𝜓   ▶   𝜒   )
21dfvd2i 44583 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 44584 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   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-vd2 44576
This theorem is referenced by:  e2bi  44630  e2bir  44631  sspwtr  44819  pwtrVD  44822  pwtrrVD  44823  suctrALT2VD  44834  tpid3gVD  44840  en3lplem1VD  44841  3ornot23VD  44845  orbi1rVD  44846  19.21a3con13vVD  44850  tratrbVD  44859  syl5impVD  44861  ssralv2VD  44864  truniALTVD  44876  trintALTVD  44878  onfrALTlem3VD  44885  onfrALTlem2VD  44887  onfrALTlem1VD  44888  relopabVD  44899  19.41rgVD  44900  hbimpgVD  44902  ax6e2eqVD  44905  ax6e2ndeqVD  44907  sb5ALTVD  44911  vk15.4jVD  44912  con3ALTVD  44914
  Copyright terms: Public domain W3C validator