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 44656
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 44605 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 406 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 44605 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 406 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 44605 . . . . . . . 8 (𝜑 → (𝜓𝜃))
98imp 406 . . . . . . 7 ((𝜑𝜓) → 𝜃)
10 e222.4 . . . . . . 7 (𝜒 → (𝜃 → (𝜏𝜂)))
116, 9, 10syl2im 40 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜓) → (𝜏𝜂)))
1211pm2.43i 52 . . . . 5 ((𝜑𝜓) → (𝜏𝜂))
133, 12syl5com 31 . . . 4 ((𝜑𝜓) → ((𝜑𝜓) → 𝜂))
1413pm2.43i 52 . . 3 ((𝜑𝜓) → 𝜂)
1514ex 412 . 2 (𝜑 → (𝜓𝜂))
1615dfvd2ir 44606 1 (   𝜑   ,   𝜓   ▶   𝜂   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  (   wvd2 44597
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 207  df-an 396  df-vd2 44598
This theorem is referenced by:  e220  44657  e202  44659  e022  44661  e002  44663  e020  44665  e200  44667  e221  44669  e212  44671  e122  44673  e112  44674  e121  44676  e211  44677  e22  44691  suctrALT2VD  44856  en3lplem2VD  44864  19.21a3con13vVD  44872  tratrbVD  44881
  Copyright terms: Public domain W3C validator