Proof of Theorem bj-peircestab
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → ((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓)) |
2 | 1 | a2i 14 |
. . 3
⊢
((((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → (((𝜑 → 𝜓) → 𝜓) → 𝜑)) → (((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)) |
3 | | ax-1 6 |
. . . . . . 7
⊢ (𝜓 → ((𝜑 → 𝜓) → 𝜓)) |
4 | 3 | imim2i 16 |
. . . . . 6
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → ((((𝜑 → 𝜓) → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓))) |
5 | | peirce 204 |
. . . . . 6
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → ((𝜑 → 𝜓) → 𝜓)) → ((𝜑 → 𝜓) → 𝜓)) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) |
7 | | imim2 58 |
. . . . 5
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜓) → 𝜓) → ((𝜑 → 𝜓) → 𝜑))) |
8 | | peirce 204 |
. . . . 5
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑) |
9 | 6, 7, 8 | syl56 36 |
. . . 4
⊢ ((𝜓 → 𝜑) → (((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜑)) |
10 | 9 | a1dd 50 |
. . 3
⊢ ((𝜓 → 𝜑) → (((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → (((𝜑 → 𝜓) → 𝜓) → 𝜑))) |
11 | 2, 10 | syl11 33 |
. 2
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → ((𝜓 → 𝜑) → 𝜓)) |
12 | | peirce 204 |
. 2
⊢ (((𝜓 → 𝜑) → 𝜓) → 𝜓) |
13 | 11, 12 | syl 17 |
1
⊢
(((((𝜑 → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓) |