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 42251
Description: A virtual deduction elimination rule. syl6 35 is e2 42251 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 42205 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 42206 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 42197
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 42198
This theorem is referenced by:  e2bi  42252  e2bir  42253  sspwtr  42441  pwtrVD  42444  pwtrrVD  42445  suctrALT2VD  42456  tpid3gVD  42462  en3lplem1VD  42463  3ornot23VD  42467  orbi1rVD  42468  19.21a3con13vVD  42472  tratrbVD  42481  syl5impVD  42483  ssralv2VD  42486  truniALTVD  42498  trintALTVD  42500  onfrALTlem3VD  42507  onfrALTlem2VD  42509  onfrALTlem1VD  42510  relopabVD  42521  19.41rgVD  42522  hbimpgVD  42524  ax6e2eqVD  42527  ax6e2ndeqVD  42529  sb5ALTVD  42533  vk15.4jVD  42534  con3ALTVD  42536
  Copyright terms: Public domain W3C validator