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 37877
Description: A virtual deduction elimination rule. syl6 34 is e2 37877 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 37822 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 34 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 37823 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 37814
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 196  df-an 385  df-vd2 37815
This theorem is referenced by:  e2bi  37878  e2bir  37879  sspwtr  38070  pwtrVD  38081  pwtrrVD  38082  suctrALT2VD  38093  tpid3gVD  38099  en3lplem1VD  38100  3ornot23VD  38104  orbi1rVD  38105  19.21a3con13vVD  38109  tratrbVD  38119  syl5impVD  38121  ssralv2VD  38124  truniALTVD  38136  trintALTVD  38138  onfrALTlem3VD  38145  onfrALTlem2VD  38147  onfrALTlem1VD  38148  relopabVD  38159  19.41rgVD  38160  hbimpgVD  38162  ax6e2eqVD  38165  ax6e2ndeqVD  38167  sb5ALTVD  38171  vk15.4jVD  38172  con3ALTVD  38174
  Copyright terms: Public domain W3C validator