Proof of Theorem dflb2s
Step | Hyp | Ref
| Expression |
1 | | ax-init 7 |
. . . . . 6
⊦ (~ (𝜑 ⊸ 𝜓) ⅋
(𝜑 ⊸ 𝜓)) |
2 | 1 | dfli1 63 |
. . . . 5
⊦ (~ (𝜑 ⊸ 𝜓) ⅋
(~ 𝜑 ⅋ 𝜓)) |
3 | 2 | dfli2i 66 |
. . . 4
⊦ ((𝜑 ⊸ 𝜓) ⊸
(~ 𝜑 ⅋ 𝜓)) |
4 | 3 | acm1s 84 |
. . 3
⊦ (((𝜑 ⊸ 𝜓) &
(𝜓 ⊸ 𝜑))
⊸ ((~ 𝜑 ⅋ 𝜓) & (𝜓 ⊸
𝜑))) |
5 | | ax-init 7 |
. . . . . 6
⊦ (~ (𝜓 ⊸ 𝜑) ⅋
(𝜓 ⊸ 𝜑)) |
6 | 5 | dfli1 63 |
. . . . 5
⊦ (~ (𝜓 ⊸ 𝜑) ⅋
(~ 𝜓 ⅋ 𝜑)) |
7 | 6 | dfli2i 66 |
. . . 4
⊦ ((𝜓 ⊸ 𝜑) ⊸
(~ 𝜓 ⅋ 𝜑)) |
8 | 7 | acm2s 85 |
. . 3
⊦ (((~ 𝜑 ⅋ 𝜓) &
(𝜓 ⊸ 𝜑))
⊸ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋
𝜑))) |
9 | 4, 8 | syl 75 |
. 2
⊦ (((𝜑 ⊸ 𝜓) &
(𝜓 ⊸ 𝜑))
⊸ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋
𝜑))) |
10 | | df-lb 56 |
. . . 4
⊦ ((~ (𝜑 ⧟ 𝜓) ⅋
((~ 𝜑 ⅋ 𝜓)
& (~ 𝜓 ⅋ 𝜑))) & (~ ((~ 𝜑
⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑)) ⅋
(𝜑 ⧟ 𝜓))) |
11 | 10 | eac2i 40 |
. . 3
⊦ (~ ((~ 𝜑 ⅋ 𝜓) & (~
𝜓 ⅋ 𝜑))
⅋ (𝜑 ⧟ 𝜓)) |
12 | 11 | dfli2i 66 |
. 2
⊦ (((~ 𝜑 ⅋ 𝜓) & (~
𝜓 ⅋ 𝜑))
⊸ (𝜑 ⧟ 𝜓)) |
13 | 9, 12 | syl 75 |
1
⊦ (((𝜑 ⊸ 𝜓) &
(𝜓 ⊸ 𝜑))
⊸ (𝜑 ⧟ 𝜓)) |