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 40968
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 40917 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 409 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 40917 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 409 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 40917 . . . . . . . 8 (𝜑 → (𝜓𝜃))
98imp 409 . . . . . . 7 ((𝜑𝜓) → 𝜃)
10 e222.4 . . . . . . 7 (𝜒 → (𝜃 → (𝜏𝜂)))
116, 9, 10syl2im 40 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜓) → (𝜏𝜂)))
1211pm2.43i 52 . . . . 5 ((𝜑𝜓) → (𝜏𝜂))
133, 12syl5com 31 . . . 4 ((𝜑𝜓) → ((𝜑𝜓) → 𝜂))
1413pm2.43i 52 . . 3 ((𝜑𝜓) → 𝜂)
1514ex 415 . 2 (𝜑 → (𝜓𝜂))
1615dfvd2ir 40918 1 (   𝜑   ,   𝜓   ▶   𝜂   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  (   wvd2 40909
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 40910
This theorem is referenced by:  e220  40969  e202  40971  e022  40973  e002  40975  e020  40977  e200  40979  e221  40981  e212  40983  e122  40985  e112  40986  e121  40988  e211  40989  e22  41003  suctrALT2VD  41168  en3lplem2VD  41176  19.21a3con13vVD  41184  tratrbVD  41193
  Copyright terms: Public domain W3C validator