Proof of Theorem lbi2s
Step | Hyp | Ref
| Expression |
1 | | df-lb 56 |
. . . . 5
⊦ ((~ (𝜑 ⧟ 𝜓) ⅋
((~ 𝜑 ⅋ 𝜓)
& (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑
⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋
(𝜑 ⧟ 𝜓))) |
2 | 1 | eac1i 38 |
. . . 4
⊦ (~ (𝜑 ⧟ 𝜓) ⅋
((~ 𝜑 ⅋ 𝜓)
& (~ 𝜓 ⅋ 𝜑))) |
3 | 2 | ax-eac2 34 |
. . 3
⊦ (~ (𝜑 ⧟ 𝜓) ⅋
(~ 𝜓 ⅋ 𝜑)) |
4 | | df-li 62 |
. . . 4
⊦ ((𝜓 ⊸ 𝜑) ⧟
(~ 𝜓 ⅋ 𝜑)) |
5 | | df-lb 56 |
. . . . . 6
⊦ ((~ ((𝜓 ⊸ 𝜑) ⧟
(~ 𝜓 ⅋ 𝜑))
⅋ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓
⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋
(𝜓 ⊸ 𝜑))))
& (~ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓
⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋
(𝜓 ⊸ 𝜑)))
⅋ ((𝜓 ⊸ 𝜑) ⧟ (~ 𝜓
⅋ 𝜑)))) |
6 | 5 | eac1i 38 |
. . . . 5
⊦ (~ ((𝜓 ⊸ 𝜑) ⧟
(~ 𝜓 ⅋ 𝜑))
⅋ ((~ (𝜓 ⊸ 𝜑) ⅋ (~ 𝜓
⅋ 𝜑)) & (~ (~ 𝜓 ⅋ 𝜑) ⅋
(𝜓 ⊸ 𝜑)))) |
7 | 6 | ax-eac2 34 |
. . . 4
⊦ (~ ((𝜓 ⊸ 𝜑) ⧟
(~ 𝜓 ⅋ 𝜑))
⅋ (~ (~ 𝜓 ⅋ 𝜑) ⅋ (𝜓 ⊸
𝜑))) |
8 | 4, 7 | cut1 10 |
. . 3
⊦ (~ (~ 𝜓 ⅋ 𝜑) ⅋
(𝜓 ⊸ 𝜑)) |
9 | 3, 8 | ax-cut 6 |
. 2
⊦ (~ (𝜑 ⧟ 𝜓) ⅋
(𝜓 ⊸ 𝜑)) |
10 | | df-li 62 |
. 2
⊦ (((𝜑 ⧟ 𝜓) ⊸
(𝜓 ⊸ 𝜑))
⧟ (~ (𝜑 ⧟ 𝜓) ⅋ (𝜓 ⊸
𝜑))) |
11 | 9, 10 | lb2i 60 |
1
⊦ ((𝜑 ⧟ 𝜓) ⊸
(𝜓 ⊸ 𝜑)) |