Proof of Theorem rblem6
Step | Hyp | Ref
| Expression |
1 | | rblem6.1 |
. 2
⊢ ¬
(¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) |
2 | | rb-ax4 1762 |
. . . . . . 7
⊢ (¬
(¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) |
3 | | rb-ax3 1761 |
. . . . . . 7
⊢ (¬
¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓))) |
4 | 2, 3 | rbsyl 1763 |
. . . . . 6
⊢ (¬
¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) |
5 | | rb-ax2 1760 |
. . . . . 6
⊢ (¬
(¬ ¬ (¬ 𝜑 ∨
𝜓) ∨ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓))) |
6 | 4, 5 | anmp 1758 |
. . . . 5
⊢ (¬
(¬ 𝜑 ∨ 𝜓) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓)) |
7 | | rblem3 1766 |
. . . . 5
⊢ (¬
(¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ ((¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓))) |
8 | 6, 7 | anmp 1758 |
. . . 4
⊢ ((¬
(¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓)) |
9 | | rb-ax2 1760 |
. . . 4
⊢ (¬
((¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) ∨ ¬ ¬ (¬ 𝜑 ∨ 𝜓)) ∨ (¬ ¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)))) |
10 | 8, 9 | anmp 1758 |
. . 3
⊢ (¬
¬ (¬ 𝜑 ∨ 𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑))) |
11 | | rblem5 1768 |
. . 3
⊢ (¬
(¬ ¬ (¬ 𝜑 ∨
𝜓) ∨ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑))) ∨ (¬ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) ∨ (¬ 𝜑 ∨ 𝜓))) |
12 | 10, 11 | anmp 1758 |
. 2
⊢ (¬
¬ (¬ (¬ 𝜑 ∨
𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)) ∨ (¬ 𝜑 ∨ 𝜓)) |
13 | 1, 12 | anmp 1758 |
1
⊢ (¬
𝜑 ∨ 𝜓) |