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 41789
Description: A virtual deduction elimination rule. syl6 35 is e2 41789 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 41743 . . 3 (𝜑 → (𝜓𝜒))
3 e2.2 . . 3 (𝜒𝜃)
42, 3syl6 35 . 2 (𝜑 → (𝜓𝜃))
54dfvd2ir 41744 1 (   𝜑   ,   𝜓   ▶   𝜃   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  (   wvd2 41735
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 210  df-an 400  df-vd2 41736
This theorem is referenced by:  e2bi  41790  e2bir  41791  sspwtr  41979  pwtrVD  41982  pwtrrVD  41983  suctrALT2VD  41994  tpid3gVD  42000  en3lplem1VD  42001  3ornot23VD  42005  orbi1rVD  42006  19.21a3con13vVD  42010  tratrbVD  42019  syl5impVD  42021  ssralv2VD  42024  truniALTVD  42036  trintALTVD  42038  onfrALTlem3VD  42045  onfrALTlem2VD  42047  onfrALTlem1VD  42048  relopabVD  42059  19.41rgVD  42060  hbimpgVD  42062  ax6e2eqVD  42065  ax6e2ndeqVD  42067  sb5ALTVD  42071  vk15.4jVD  42072  con3ALTVD  42074
  Copyright terms: Public domain W3C validator