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 38682
Description: A virtual deduction elimination rule. syl6 35 is e2 38682 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 38627 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 38628 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 38619
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 197  df-an 386  df-vd2 38620
This theorem is referenced by:  e2bi  38683  e2bir  38684  sspwtr  38874  pwtrVD  38885  pwtrrVD  38886  suctrALT2VD  38897  tpid3gVD  38903  en3lplem1VD  38904  3ornot23VD  38908  orbi1rVD  38909  19.21a3con13vVD  38913  tratrbVD  38923  syl5impVD  38925  ssralv2VD  38928  truniALTVD  38940  trintALTVD  38942  onfrALTlem3VD  38949  onfrALTlem2VD  38951  onfrALTlem1VD  38952  relopabVD  38963  19.41rgVD  38964  hbimpgVD  38966  ax6e2eqVD  38969  ax6e2ndeqVD  38971  sb5ALTVD  38975  vk15.4jVD  38976  con3ALTVD  38978
  Copyright terms: Public domain W3C validator