Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e222 Structured version   Visualization version   GIF version

Theorem e222 39809
 Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e222.1 (   𝜑   ,   𝜓   ▶   𝜒   )
e222.2 (   𝜑   ,   𝜓   ▶   𝜃   )
e222.3 (   𝜑   ,   𝜓   ▶   𝜏   )
e222.4 (𝜒 → (𝜃 → (𝜏𝜂)))
Assertion
Ref Expression
e222 (   𝜑   ,   𝜓   ▶   𝜂   )

Proof of Theorem e222
StepHypRef Expression
1 e222.3 . . . . . . 7 (   𝜑   ,   𝜓   ▶   𝜏   )
21dfvd2i 39749 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 397 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 39749 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 397 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 39749 . . . . . . . 8 (𝜑 → (𝜓𝜃))
98imp 397 . . . . . . 7 ((𝜑𝜓) → 𝜃)
10 e222.4 . . . . . . 7 (𝜒 → (𝜃 → (𝜏𝜂)))
116, 9, 10syl2im 40 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜓) → (𝜏𝜂)))
1211pm2.43i 52 . . . . 5 ((𝜑𝜓) → (𝜏𝜂))
133, 12syl5com 31 . . . 4 ((𝜑𝜓) → ((𝜑𝜓) → 𝜂))
1413pm2.43i 52 . . 3 ((𝜑𝜓) → 𝜂)
1514ex 403 . 2 (𝜑 → (𝜓𝜂))
1615dfvd2ir 39750 1 (   𝜑   ,   𝜓   ▶   𝜂   )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386  (   wvd2 39741 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 199  df-an 387  df-vd2 39742 This theorem is referenced by:  e220  39810  e202  39812  e022  39814  e002  39816  e020  39818  e200  39820  e221  39822  e212  39824  e122  39826  e112  39827  e121  39829  e211  39830  e22  39844  suctrALT2VD  40009  en3lplem2VD  40017  19.21a3con13vVD  40025  tratrbVD  40034
 Copyright terms: Public domain W3C validator