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 44651
Description: A virtual deduction elimination rule. syl6 35 is e2 44651 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 44605 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 44606 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 44597
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 44598
This theorem is referenced by:  e2bi  44652  e2bir  44653  sspwtr  44841  pwtrVD  44844  pwtrrVD  44845  suctrALT2VD  44856  tpid3gVD  44862  en3lplem1VD  44863  3ornot23VD  44867  orbi1rVD  44868  19.21a3con13vVD  44872  tratrbVD  44881  syl5impVD  44883  ssralv2VD  44886  truniALTVD  44898  trintALTVD  44900  onfrALTlem3VD  44907  onfrALTlem2VD  44909  onfrALTlem1VD  44910  relopabVD  44921  19.41rgVD  44922  hbimpgVD  44924  ax6e2eqVD  44927  ax6e2ndeqVD  44929  sb5ALTVD  44933  vk15.4jVD  44934  con3ALTVD  44936
  Copyright terms: Public domain W3C validator