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 43382
Description: A virtual deduction elimination rule. syl6 35 is e2 43382 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 43336 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 43337 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 43328
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 206  df-an 397  df-vd2 43329
This theorem is referenced by:  e2bi  43383  e2bir  43384  sspwtr  43572  pwtrVD  43575  pwtrrVD  43576  suctrALT2VD  43587  tpid3gVD  43593  en3lplem1VD  43594  3ornot23VD  43598  orbi1rVD  43599  19.21a3con13vVD  43603  tratrbVD  43612  syl5impVD  43614  ssralv2VD  43617  truniALTVD  43629  trintALTVD  43631  onfrALTlem3VD  43638  onfrALTlem2VD  43640  onfrALTlem1VD  43641  relopabVD  43652  19.41rgVD  43653  hbimpgVD  43655  ax6e2eqVD  43658  ax6e2ndeqVD  43660  sb5ALTVD  43664  vk15.4jVD  43665  con3ALTVD  43667
  Copyright terms: Public domain W3C validator