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

Theorem e222 39382
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 39322 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 444 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 39322 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 444 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 39322 . . . . . . . 8 (𝜑 → (𝜓𝜃))
98imp 444 . . . . . . 7 ((𝜑𝜓) → 𝜃)
10 e222.4 . . . . . . 7 (𝜒 → (𝜃 → (𝜏𝜂)))
116, 9, 10syl2im 40 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜓) → (𝜏𝜂)))
1211pm2.43i 52 . . . . 5 ((𝜑𝜓) → (𝜏𝜂))
133, 12syl5com 31 . . . 4 ((𝜑𝜓) → ((𝜑𝜓) → 𝜂))
1413pm2.43i 52 . . 3 ((𝜑𝜓) → 𝜂)
1514ex 449 . 2 (𝜑 → (𝜓𝜂))
1615dfvd2ir 39323 1 (   𝜑   ,   𝜓   ▶   𝜂   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  (   wvd2 39314
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 197  df-an 385  df-vd2 39315
This theorem is referenced by:  e220  39383  e202  39385  e022  39387  e002  39389  e020  39391  e200  39393  e221  39395  e212  39397  e122  39399  e112  39400  e121  39402  e211  39403  e22  39417  suctrALT2VD  39589  en3lplem2VD  39597  19.21a3con13vVD  39605  tratrbVD  39615
  Copyright terms: Public domain W3C validator