MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  re2luk1 Structured version   Visualization version   GIF version

Theorem re2luk1 1688
Description: luk-1 1578 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
re2luk1 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))

Proof of Theorem re2luk1
StepHypRef Expression
1 rb-imdf 1673 . . . 4 ¬ (¬ (¬ ((𝜓𝜒) → (𝜑𝜒)) ∨ (¬ (𝜓𝜒) ∨ (𝜑𝜒))) ∨ ¬ (¬ (¬ (𝜓𝜒) ∨ (𝜑𝜒)) ∨ ((𝜓𝜒) → (𝜑𝜒))))
21rblem7 1686 . . 3 (¬ (¬ (𝜓𝜒) ∨ (𝜑𝜒)) ∨ ((𝜓𝜒) → (𝜑𝜒)))
3 rb-imdf 1673 . . . . . . . 8 ¬ (¬ (¬ (𝜓𝜒) ∨ (¬ 𝜓𝜒)) ∨ ¬ (¬ (¬ 𝜓𝜒) ∨ (𝜓𝜒)))
43rblem6 1685 . . . . . . 7 (¬ (𝜓𝜒) ∨ (¬ 𝜓𝜒))
5 rb-ax2 1676 . . . . . . . 8 (¬ (¬ (𝜓𝜒) ∨ ¬ ¬ (¬ 𝜓𝜒)) ∨ (¬ ¬ (¬ 𝜓𝜒) ∨ ¬ (𝜓𝜒)))
6 rb-ax4 1678 . . . . . . . . . 10 (¬ (¬ (𝜓𝜒) ∨ ¬ (𝜓𝜒)) ∨ ¬ (𝜓𝜒))
7 rb-ax3 1677 . . . . . . . . . 10 (¬ ¬ (𝜓𝜒) ∨ (¬ (𝜓𝜒) ∨ ¬ (𝜓𝜒)))
86, 7rbsyl 1679 . . . . . . . . 9 (¬ ¬ (𝜓𝜒) ∨ ¬ (𝜓𝜒))
9 rb-ax4 1678 . . . . . . . . . . 11 (¬ (¬ (¬ 𝜓𝜒) ∨ ¬ (¬ 𝜓𝜒)) ∨ ¬ (¬ 𝜓𝜒))
10 rb-ax3 1677 . . . . . . . . . . 11 (¬ ¬ (¬ 𝜓𝜒) ∨ (¬ (¬ 𝜓𝜒) ∨ ¬ (¬ 𝜓𝜒)))
119, 10rbsyl 1679 . . . . . . . . . 10 (¬ ¬ (¬ 𝜓𝜒) ∨ ¬ (¬ 𝜓𝜒))
12 rb-ax2 1676 . . . . . . . . . 10 (¬ (¬ ¬ (¬ 𝜓𝜒) ∨ ¬ (¬ 𝜓𝜒)) ∨ (¬ (¬ 𝜓𝜒) ∨ ¬ ¬ (¬ 𝜓𝜒)))
1311, 12anmp 1674 . . . . . . . . 9 (¬ (¬ 𝜓𝜒) ∨ ¬ ¬ (¬ 𝜓𝜒))
148, 13rblem1 1680 . . . . . . . 8 (¬ (¬ (𝜓𝜒) ∨ (¬ 𝜓𝜒)) ∨ (¬ (𝜓𝜒) ∨ ¬ ¬ (¬ 𝜓𝜒)))
155, 14rbsyl 1679 . . . . . . 7 (¬ (¬ (𝜓𝜒) ∨ (¬ 𝜓𝜒)) ∨ (¬ ¬ (¬ 𝜓𝜒) ∨ ¬ (𝜓𝜒)))
164, 15anmp 1674 . . . . . 6 (¬ ¬ (¬ 𝜓𝜒) ∨ ¬ (𝜓𝜒))
17 rb-imdf 1673 . . . . . . 7 ¬ (¬ (¬ (𝜑𝜒) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ (¬ 𝜑𝜒) ∨ (𝜑𝜒)))
1817rblem7 1686 . . . . . 6 (¬ (¬ 𝜑𝜒) ∨ (𝜑𝜒))
1916, 18rblem1 1680 . . . . 5 (¬ (¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒)) ∨ (¬ (𝜓𝜒) ∨ (𝜑𝜒)))
20 rb-ax1 1675 . . . . . 6 (¬ (¬ 𝜓𝜒) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒)))
21 rb-ax2 1676 . . . . . . 7 (¬ ((¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ 𝜑𝜓)) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒))))
22 rb-ax4 1678 . . . . . . . . . 10 (¬ (¬ (¬ 𝜑𝜓) ∨ ¬ (¬ 𝜑𝜓)) ∨ ¬ (¬ 𝜑𝜓))
23 rb-ax3 1677 . . . . . . . . . 10 (¬ ¬ (¬ 𝜑𝜓) ∨ (¬ (¬ 𝜑𝜓) ∨ ¬ (¬ 𝜑𝜓)))
2422, 23rbsyl 1679 . . . . . . . . 9 (¬ ¬ (¬ 𝜑𝜓) ∨ ¬ (¬ 𝜑𝜓))
25 rb-ax4 1678 . . . . . . . . . 10 (¬ ((¬ 𝜑𝜒) ∨ (¬ 𝜑𝜒)) ∨ (¬ 𝜑𝜒))
26 rb-ax3 1677 . . . . . . . . . 10 (¬ (¬ 𝜑𝜒) ∨ ((¬ 𝜑𝜒) ∨ (¬ 𝜑𝜒)))
2725, 26rbsyl 1679 . . . . . . . . 9 (¬ (¬ 𝜑𝜒) ∨ (¬ 𝜑𝜒))
2824, 27, 11rblem4 1683 . . . . . . . 8 (¬ ((¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ 𝜓𝜒)) ∨ ((¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ 𝜑𝜓)))
29 rb-ax2 1676 . . . . . . . 8 (¬ (¬ (¬ 𝜓𝜒) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒))) ∨ ((¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ 𝜓𝜒)))
3028, 29rbsyl 1679 . . . . . . 7 (¬ (¬ (¬ 𝜓𝜒) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒))) ∨ ((¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒)) ∨ ¬ (¬ 𝜑𝜓)))
3121, 30rbsyl 1679 . . . . . 6 (¬ (¬ (¬ 𝜓𝜒) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ 𝜑𝜒))) ∨ (¬ (¬ 𝜑𝜓) ∨ (¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒))))
3220, 31anmp 1674 . . . . 5 (¬ (¬ 𝜑𝜓) ∨ (¬ (¬ 𝜓𝜒) ∨ (¬ 𝜑𝜒)))
3319, 32rbsyl 1679 . . . 4 (¬ (¬ 𝜑𝜓) ∨ (¬ (𝜓𝜒) ∨ (𝜑𝜒)))
34 rb-imdf 1673 . . . . 5 ¬ (¬ (¬ (𝜑𝜓) ∨ (¬ 𝜑𝜓)) ∨ ¬ (¬ (¬ 𝜑𝜓) ∨ (𝜑𝜓)))
3534rblem6 1685 . . . 4 (¬ (𝜑𝜓) ∨ (¬ 𝜑𝜓))
3633, 35rbsyl 1679 . . 3 (¬ (𝜑𝜓) ∨ (¬ (𝜓𝜒) ∨ (𝜑𝜒)))
372, 36rbsyl 1679 . 2 (¬ (𝜑𝜓) ∨ ((𝜓𝜒) → (𝜑𝜒)))
38 rb-imdf 1673 . . 3 ¬ (¬ (¬ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))) ∨ (¬ (𝜑𝜓) ∨ ((𝜓𝜒) → (𝜑𝜒)))) ∨ ¬ (¬ (¬ (𝜑𝜓) ∨ ((𝜓𝜒) → (𝜑𝜒))) ∨ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))))
3938rblem7 1686 . 2 (¬ (¬ (𝜑𝜓) ∨ ((𝜓𝜒) → (𝜑𝜒))) ∨ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))))
4037, 39anmp 1674 1 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383
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-or 385  df-an 386
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator