Proof of Theorem mdasr
Step | Hyp | Ref
| Expression |
1 | | ax-mdco 8 |
. . . . 5
⊦ (~ (𝜑 ⅋ (𝜓 ⅋
𝜒)) ⅋ ((𝜓
⅋ 𝜒) ⅋ 𝜑)) |
2 | | ax-mdas 9 |
. . . . 5
⊦ (~ ((𝜓 ⅋ 𝜒) ⅋
𝜑) ⅋ (𝜓
⅋ (𝜒 ⅋ 𝜑))) |
3 | 1, 2 | ax-cut 6 |
. . . 4
⊦ (~ (𝜑 ⅋ (𝜓 ⅋
𝜒)) ⅋ (𝜓
⅋ (𝜒 ⅋ 𝜑))) |
4 | | ax-mdco 8 |
. . . 4
⊦ (~ (𝜓 ⅋ (𝜒 ⅋
𝜑)) ⅋ ((𝜒
⅋ 𝜑) ⅋ 𝜓)) |
5 | 3, 4 | ax-cut 6 |
. . 3
⊦ (~ (𝜑 ⅋ (𝜓 ⅋
𝜒)) ⅋ ((𝜒
⅋ 𝜑) ⅋ 𝜓)) |
6 | | ax-mdas 9 |
. . 3
⊦ (~ ((𝜒 ⅋ 𝜑) ⅋
𝜓) ⅋ (𝜒
⅋ (𝜑 ⅋ 𝜓))) |
7 | 5, 6 | ax-cut 6 |
. 2
⊦ (~ (𝜑 ⅋ (𝜓 ⅋
𝜒)) ⅋ (𝜒
⅋ (𝜑 ⅋ 𝜓))) |
8 | | ax-mdco 8 |
. 2
⊦ (~ (𝜒 ⅋ (𝜑 ⅋
𝜓)) ⅋ ((𝜑
⅋ 𝜓) ⅋ 𝜒)) |
9 | 7, 8 | ax-cut 6 |
1
⊦ (~ (𝜑 ⅋ (𝜓 ⅋
𝜒)) ⅋ ((𝜑
⅋ 𝜓) ⅋ 𝜒)) |