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 39173
Description: A virtual deduction elimination rule. syl6 35 is e2 39173 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 39118 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 39119 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 39110
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 385  df-vd2 39111
This theorem is referenced by:  e2bi  39174  e2bir  39175  sspwtr  39365  pwtrVD  39373  pwtrrVD  39374  suctrALT2VD  39385  tpid3gVD  39391  en3lplem1VD  39392  3ornot23VD  39396  orbi1rVD  39397  19.21a3con13vVD  39401  tratrbVD  39411  syl5impVD  39413  ssralv2VD  39416  truniALTVD  39428  trintALTVD  39430  onfrALTlem3VD  39437  onfrALTlem2VD  39439  onfrALTlem1VD  39440  relopabVD  39451  19.41rgVD  39452  hbimpgVD  39454  ax6e2eqVD  39457  ax6e2ndeqVD  39459  sb5ALTVD  39463  vk15.4jVD  39464  con3ALTVD  39466
  Copyright terms: Public domain W3C validator