Proof of Theorem mcco
Step | Hyp | Ref
| Expression |
1 | | dnis 78 |
. . 3
⊦ ((𝜑 ⊗ 𝜓) ⊸
~ ~ (𝜑 ⊗ 𝜓)) |
2 | | ax-mdco 8 |
. . . . . 6
⊦ (~ (~ 𝜓 ⅋ ~ 𝜑)
⅋ (~ 𝜑 ⅋ ~ 𝜓)) |
3 | 2 | dfli2i 66 |
. . . . 5
⊦ ((~ 𝜓 ⅋ ~ 𝜑)
⊸ (~ 𝜑 ⅋ ~ 𝜓)) |
4 | | dnis 78 |
. . . . . 6
⊦ ((~ 𝜑 ⅋ ~ 𝜓)
⊸ ~ ~ (~ 𝜑 ⅋ ~ 𝜓)) |
5 | | id 77 |
. . . . . . . 8
⊦ ((𝜑 ⊗ 𝜓) ⊸
(𝜑 ⊗ 𝜓)) |
6 | | df-mc 106 |
. . . . . . . 8
⊦ ((𝜑 ⊗ 𝜓) ⧟
~ (~ 𝜑 ⅋ ~ 𝜓)) |
7 | 5, 6 | lb1s 67 |
. . . . . . 7
⊦ ((𝜑 ⊗ 𝜓) ⊸
~ (~ 𝜑 ⅋ ~ 𝜓)) |
8 | | licon 94 |
. . . . . . 7
⊦ (((𝜑 ⊗ 𝜓) ⊸
~ (~ 𝜑 ⅋ ~ 𝜓)) ⊸ (~ ~ (~ 𝜑
⅋ ~ 𝜓) ⊸ ~ (𝜑 ⊗ 𝜓))) |
9 | 7, 8 | lmp 76 |
. . . . . 6
⊦ (~ ~ (~ 𝜑 ⅋ ~ 𝜓)
⊸ ~ (𝜑 ⊗ 𝜓)) |
10 | 4, 9 | syl 75 |
. . . . 5
⊦ ((~ 𝜑 ⅋ ~ 𝜓)
⊸ ~ (𝜑 ⊗ 𝜓)) |
11 | 3, 10 | syl 75 |
. . . 4
⊦ ((~ 𝜓 ⅋ ~ 𝜑)
⊸ ~ (𝜑 ⊗ 𝜓)) |
12 | | licon 94 |
. . . 4
⊦ (((~ 𝜓 ⅋ ~ 𝜑)
⊸ ~ (𝜑 ⊗ 𝜓)) ⊸ (~ ~ (𝜑
⊗ 𝜓) ⊸ ~ (~ 𝜓 ⅋ ~ 𝜑))) |
13 | 11, 12 | lmp 76 |
. . 3
⊦ (~ ~ (𝜑 ⊗ 𝜓) ⊸
~ (~ 𝜓 ⅋ ~ 𝜑)) |
14 | 1, 13 | syl 75 |
. 2
⊦ ((𝜑 ⊗ 𝜓) ⊸
~ (~ 𝜓 ⅋ ~ 𝜑)) |
15 | | df-mc 106 |
. 2
⊦ ((𝜓 ⊗ 𝜑) ⧟
~ (~ 𝜓 ⅋ ~ 𝜑)) |
16 | 14, 15 | lb2s 68 |
1
⊦ ((𝜑 ⊗ 𝜓) ⊸
(𝜓 ⊗ 𝜑)) |