Proof of Theorem rblem5
Step | Hyp | Ref
| Expression |
1 | | rb-ax2 1756 |
. 2
⊢ (¬
(𝜑 ∨ ¬ ¬ 𝜓) ∨ (¬ ¬ 𝜓 ∨ 𝜑)) |
2 | | rb-ax4 1758 |
. . . . 5
⊢ (¬
(𝜑 ∨ 𝜑) ∨ 𝜑) |
3 | | rb-ax3 1757 |
. . . . 5
⊢ (¬
𝜑 ∨ (𝜑 ∨ 𝜑)) |
4 | 2, 3 | rbsyl 1759 |
. . . 4
⊢ (¬
𝜑 ∨ 𝜑) |
5 | | rb-ax4 1758 |
. . . . . . 7
⊢ (¬
(¬ ¬ 𝜑 ∨ ¬
¬ 𝜑) ∨ ¬ ¬
𝜑) |
6 | | rb-ax3 1757 |
. . . . . . 7
⊢ (¬
¬ ¬ 𝜑 ∨ (¬
¬ 𝜑 ∨ ¬ ¬
𝜑)) |
7 | 5, 6 | rbsyl 1759 |
. . . . . 6
⊢ (¬
¬ ¬ 𝜑 ∨ ¬
¬ 𝜑) |
8 | | rb-ax2 1756 |
. . . . . 6
⊢ (¬
(¬ ¬ ¬ 𝜑 ∨
¬ ¬ 𝜑) ∨ (¬
¬ 𝜑 ∨ ¬ ¬
¬ 𝜑)) |
9 | 7, 8 | anmp 1754 |
. . . . 5
⊢ (¬
¬ 𝜑 ∨ ¬ ¬
¬ 𝜑) |
10 | 9, 4 | rblem1 1760 |
. . . 4
⊢ (¬
(¬ 𝜑 ∨ 𝜑) ∨ (¬ ¬ ¬ 𝜑 ∨ 𝜑)) |
11 | 4, 10 | anmp 1754 |
. . 3
⊢ (¬
¬ ¬ 𝜑 ∨ 𝜑) |
12 | | rb-ax4 1758 |
. . . . 5
⊢ (¬
(¬ 𝜓 ∨ ¬ 𝜓) ∨ ¬ 𝜓) |
13 | | rb-ax3 1757 |
. . . . 5
⊢ (¬
¬ 𝜓 ∨ (¬ 𝜓 ∨ ¬ 𝜓)) |
14 | 12, 13 | rbsyl 1759 |
. . . 4
⊢ (¬
¬ 𝜓 ∨ ¬ 𝜓) |
15 | | rb-ax2 1756 |
. . . 4
⊢ (¬
(¬ ¬ 𝜓 ∨ ¬
𝜓) ∨ (¬ 𝜓 ∨ ¬ ¬ 𝜓)) |
16 | 14, 15 | anmp 1754 |
. . 3
⊢ (¬
𝜓 ∨ ¬ ¬ 𝜓) |
17 | 11, 16 | rblem1 1760 |
. 2
⊢ (¬
(¬ ¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ∨ ¬ ¬ 𝜓)) |
18 | 1, 17 | rbsyl 1759 |
1
⊢ (¬
(¬ ¬ 𝜑 ∨ 𝜓) ∨ (¬ ¬ 𝜓 ∨ 𝜑)) |