Proof of Theorem tbwlem4
Step | Hyp | Ref
| Expression |
1 | | tbw-ax4 1710 |
. . . . 5
⊢ (⊥
→ ⊥) |
2 | | tbw-ax1 1707 |
. . . . . 6
⊢ ((𝜓 → ⊥) → ((⊥
→ ⊥) → (𝜓
→ ⊥))) |
3 | | tbwlem1 1712 |
. . . . . 6
⊢ (((𝜓 → ⊥) → ((⊥
→ ⊥) → (𝜓
→ ⊥))) → ((⊥ → ⊥) → ((𝜓 → ⊥) → (𝜓 → ⊥)))) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ ((⊥
→ ⊥) → ((𝜓
→ ⊥) → (𝜓
→ ⊥))) |
5 | 1, 4 | ax-mp 5 |
. . . 4
⊢ ((𝜓 → ⊥) → (𝜓 → ⊥)) |
6 | | tbwlem1 1712 |
. . . 4
⊢ (((𝜓 → ⊥) → (𝜓 → ⊥)) → (𝜓 → ((𝜓 → ⊥) →
⊥))) |
7 | 5, 6 | ax-mp 5 |
. . 3
⊢ (𝜓 → ((𝜓 → ⊥) →
⊥)) |
8 | | tbw-ax1 1707 |
. . . 4
⊢ (((𝜑 → ⊥) → 𝜓) → ((𝜓 → ((𝜓 → ⊥) → ⊥)) →
((𝜑 → ⊥) →
((𝜓 → ⊥) →
⊥)))) |
9 | | tbwlem1 1712 |
. . . 4
⊢ ((((𝜑 → ⊥) → 𝜓) → ((𝜓 → ((𝜓 → ⊥) → ⊥)) →
((𝜑 → ⊥) →
((𝜓 → ⊥) →
⊥)))) → ((𝜓 →
((𝜓 → ⊥) →
⊥)) → (((𝜑 →
⊥) → 𝜓) →
((𝜑 → ⊥) →
((𝜓 → ⊥) →
⊥))))) |
10 | 8, 9 | ax-mp 5 |
. . 3
⊢ ((𝜓 → ((𝜓 → ⊥) → ⊥)) →
(((𝜑 → ⊥) →
𝜓) → ((𝜑 → ⊥) → ((𝜓 → ⊥) →
⊥)))) |
11 | 7, 10 | ax-mp 5 |
. 2
⊢ (((𝜑 → ⊥) → 𝜓) → ((𝜑 → ⊥) → ((𝜓 → ⊥) →
⊥))) |
12 | | tbwlem2 1713 |
. . 3
⊢ (((𝜑 → ⊥) → ((𝜓 → ⊥) → ⊥))
→ ((((𝜑 → ⊥)
→ 𝜑) → 𝜑) → ((𝜓 → ⊥) → 𝜑))) |
13 | | tbwlem3 1714 |
. . 3
⊢
(((((𝜑 → ⊥)
→ 𝜑) → 𝜑) → ((𝜓 → ⊥) → 𝜑)) → ((𝜓 → ⊥) → 𝜑)) |
14 | 12, 13 | tbwsyl 1711 |
. 2
⊢ (((𝜑 → ⊥) → ((𝜓 → ⊥) → ⊥))
→ ((𝜓 → ⊥)
→ 𝜑)) |
15 | 11, 14 | tbwsyl 1711 |
1
⊢ (((𝜑 → ⊥) → 𝜓) → ((𝜓 → ⊥) → 𝜑)) |