Proof of Theorem re2luk1
Step | Hyp | Ref
| Expression |
1 | | rb-imdf 1758 |
. . . 4
⊢ ¬
(¬ (¬ ((𝜓 →
𝜒) → (𝜑 → 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒))) ∨ ¬ (¬ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) |
2 | 1 | rblem7 1771 |
. . 3
⊢ (¬
(¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒)) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) |
3 | | rb-imdf 1758 |
. . . . . . . 8
⊢ ¬
(¬ (¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ ¬ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (𝜓 → 𝜒))) |
4 | 3 | rblem6 1770 |
. . . . . . 7
⊢ (¬
(𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) |
5 | | rb-ax2 1761 |
. . . . . . . 8
⊢ (¬
(¬ (𝜓 → 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒))) |
6 | | rb-ax4 1763 |
. . . . . . . . . 10
⊢ (¬
(¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒)) ∨ ¬ (𝜓 → 𝜒)) |
7 | | rb-ax3 1762 |
. . . . . . . . . 10
⊢ (¬
¬ (𝜓 → 𝜒) ∨ (¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒))) |
8 | 6, 7 | rbsyl 1764 |
. . . . . . . . 9
⊢ (¬
¬ (𝜓 → 𝜒) ∨ ¬ (𝜓 → 𝜒)) |
9 | | rb-ax4 1763 |
. . . . . . . . . . 11
⊢ (¬
(¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) |
10 | | rb-ax3 1762 |
. . . . . . . . . . 11
⊢ (¬
¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒))) |
11 | 9, 10 | rbsyl 1764 |
. . . . . . . . . 10
⊢ (¬
¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) |
12 | | rb-ax2 1761 |
. . . . . . . . . 10
⊢ (¬
(¬ ¬ (¬ 𝜓 ∨
𝜒) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒))) |
13 | 11, 12 | anmp 1759 |
. . . . . . . . 9
⊢ (¬
(¬ 𝜓 ∨ 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒)) |
14 | 8, 13 | rblem1 1765 |
. . . . . . . 8
⊢ (¬
(¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ ¬ ¬ (¬ 𝜓 ∨ 𝜒))) |
15 | 5, 14 | rbsyl 1764 |
. . . . . . 7
⊢ (¬
(¬ (𝜓 → 𝜒) ∨ (¬ 𝜓 ∨ 𝜒)) ∨ (¬ ¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒))) |
16 | 4, 15 | anmp 1759 |
. . . . . 6
⊢ (¬
¬ (¬ 𝜓 ∨ 𝜒) ∨ ¬ (𝜓 → 𝜒)) |
17 | | rb-imdf 1758 |
. . . . . . 7
⊢ ¬
(¬ (¬ (𝜑 → 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ (¬ 𝜑 ∨ 𝜒) ∨ (𝜑 → 𝜒))) |
18 | 17 | rblem7 1771 |
. . . . . 6
⊢ (¬
(¬ 𝜑 ∨ 𝜒) ∨ (𝜑 → 𝜒)) |
19 | 16, 18 | rblem1 1765 |
. . . . 5
⊢ (¬
(¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒))) |
20 | | rb-ax1 1760 |
. . . . . 6
⊢ (¬
(¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) |
21 | | rb-ax2 1761 |
. . . . . . 7
⊢ (¬
((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)))) |
22 | | rb-ax4 1763 |
. . . . . . . . . 10
⊢ (¬
(¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) |
23 | | rb-ax3 1762 |
. . . . . . . . . 10
⊢ (¬
¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓))) |
24 | 22, 23 | rbsyl 1764 |
. . . . . . . . 9
⊢ (¬
¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) |
25 | | rb-ax4 1763 |
. . . . . . . . . 10
⊢ (¬
((¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ (¬ 𝜑 ∨ 𝜒)) |
26 | | rb-ax3 1762 |
. . . . . . . . . 10
⊢ (¬
(¬ 𝜑 ∨ 𝜒) ∨ ((¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒))) |
27 | 25, 26 | rbsyl 1764 |
. . . . . . . . 9
⊢ (¬
(¬ 𝜑 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) |
28 | 24, 27, 11 | rblem4 1768 |
. . . . . . . 8
⊢ (¬
((¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒)) ∨ ((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓))) |
29 | | rb-ax2 1761 |
. . . . . . . 8
⊢ (¬
(¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜓 ∨ 𝜒))) |
30 | 28, 29 | rbsyl 1764 |
. . . . . . 7
⊢ (¬
(¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ ((¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)) ∨ ¬ (¬ 𝜑 ∨ 𝜓))) |
31 | 21, 30 | rbsyl 1764 |
. . . . . 6
⊢ (¬
(¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ 𝜑 ∨ 𝜒))) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒)))) |
32 | 20, 31 | anmp 1759 |
. . . . 5
⊢ (¬
(¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ 𝜑 ∨ 𝜒))) |
33 | 19, 32 | rbsyl 1764 |
. . . 4
⊢ (¬
(¬ 𝜑 ∨ 𝜓) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒))) |
34 | | rb-imdf 1758 |
. . . . 5
⊢ ¬
(¬ (¬ (𝜑 → 𝜓) ∨ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜑 → 𝜓))) |
35 | 34 | rblem6 1770 |
. . . 4
⊢ (¬
(𝜑 → 𝜓) ∨ (¬ 𝜑 ∨ 𝜓)) |
36 | 33, 35 | rbsyl 1764 |
. . 3
⊢ (¬
(𝜑 → 𝜓) ∨ (¬ (𝜓 → 𝜒) ∨ (𝜑 → 𝜒))) |
37 | 2, 36 | rbsyl 1764 |
. 2
⊢ (¬
(𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) |
38 | | rb-imdf 1758 |
. . 3
⊢ ¬
(¬ (¬ ((𝜑 →
𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) ∨ ¬ (¬ (¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))))) |
39 | 38 | rblem7 1771 |
. 2
⊢ (¬
(¬ (𝜑 → 𝜓) ∨ ((𝜓 → 𝜒) → (𝜑 → 𝜒))) ∨ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))) |
40 | 37, 39 | anmp 1759 |
1
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) |