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 44634
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 44583 . . . . . 6 (𝜑 → (𝜓𝜏))
32imp 406 . . . . 5 ((𝜑𝜓) → 𝜏)
4 e222.1 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜒   )
54dfvd2i 44583 . . . . . . . 8 (𝜑 → (𝜓𝜒))
65imp 406 . . . . . . 7 ((𝜑𝜓) → 𝜒)
7 e222.2 . . . . . . . . 9 (   𝜑   ,   𝜓   ▶   𝜃   )
87dfvd2i 44583 . . . . . . . 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 44584 1 (   𝜑   ,   𝜓   ▶   𝜂   )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  (   wvd2 44575
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 44576
This theorem is referenced by:  e220  44635  e202  44637  e022  44639  e002  44641  e020  44643  e200  44645  e221  44647  e212  44649  e122  44651  e112  44652  e121  44654  e211  44655  e22  44669  suctrALT2VD  44834  en3lplem2VD  44842  19.21a3con13vVD  44850  tratrbVD  44859
  Copyright terms: Public domain W3C validator