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 42823
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 42772 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 408 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 42772 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 408 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 42772 . . . . . . . 8 (𝜑 → (𝜓𝜃))
98imp 408 . . . . . . 7 ((𝜑𝜓) → 𝜃)
10 e222.4 . . . . . . 7 (𝜒 → (𝜃 → (𝜏𝜂)))
116, 9, 10syl2im 40 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜓) → (𝜏𝜂)))
1211pm2.43i 52 . . . . 5 ((𝜑𝜓) → (𝜏𝜂))
133, 12syl5com 31 . . . 4 ((𝜑𝜓) → ((𝜑𝜓) → 𝜂))
1413pm2.43i 52 . . 3 ((𝜑𝜓) → 𝜂)
1514ex 414 . 2 (𝜑 → (𝜓𝜂))
1615dfvd2ir 42773 1 (   𝜑   ,   𝜓   ▶   𝜂   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  (   wvd2 42764
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 398  df-vd2 42765
This theorem is referenced by:  e220  42824  e202  42826  e022  42828  e002  42830  e020  42832  e200  42834  e221  42836  e212  42838  e122  42840  e112  42841  e121  42843  e211  42844  e22  42858  suctrALT2VD  43023  en3lplem2VD  43031  19.21a3con13vVD  43039  tratrbVD  43048
  Copyright terms: Public domain W3C validator