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 40956
Description: A virtual deduction elimination rule. syl6 35 is e2 40956 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 40910 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 40911 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 40902
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 209  df-an 399  df-vd2 40903
This theorem is referenced by:  e2bi  40957  e2bir  40958  sspwtr  41146  pwtrVD  41149  pwtrrVD  41150  suctrALT2VD  41161  tpid3gVD  41167  en3lplem1VD  41168  3ornot23VD  41172  orbi1rVD  41173  19.21a3con13vVD  41177  tratrbVD  41186  syl5impVD  41188  ssralv2VD  41191  truniALTVD  41203  trintALTVD  41205  onfrALTlem3VD  41212  onfrALTlem2VD  41214  onfrALTlem1VD  41215  relopabVD  41226  19.41rgVD  41227  hbimpgVD  41229  ax6e2eqVD  41232  ax6e2ndeqVD  41234  sb5ALTVD  41238  vk15.4jVD  41239  con3ALTVD  41241
  Copyright terms: Public domain W3C validator