Proof of Theorem luk-2
Step | Hyp | Ref
| Expression |
1 | | merlem5 1649 |
. . . . 5
⊢ ((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) |
2 | | merlem4 1648 |
. . . . 5
⊢ (((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑))) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑)) |
4 | | merlem11 1655 |
. . . 4
⊢
(((((𝜑 → ¬
(¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑)) → ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑)) |
5 | 3, 4 | ax-mp 5 |
. . 3
⊢ ((((𝜑 → ¬ (¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑) |
6 | | meredith 1644 |
. . 3
⊢
(((((𝜑 → ¬
(¬ 𝜑 → 𝜑)) → (¬ ¬ 𝜑 → ¬ (¬ 𝜑 → 𝜑))) → ¬ 𝜑) → ¬ 𝜑) → ((¬ 𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑))) |
7 | 5, 6 | ax-mp 5 |
. 2
⊢ ((¬
𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)) |
8 | | merlem11 1655 |
. 2
⊢ (((¬
𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)) → ((¬ 𝜑 → 𝜑) → 𝜑)) |
9 | 7, 8 | ax-mp 5 |
1
⊢ ((¬
𝜑 → 𝜑) → 𝜑) |