Proof of Theorem tbwlem2
Step | Hyp | Ref
| Expression |
1 | | tbw-ax4 1711 |
. . . . 5
⊢ (⊥
→ 𝜒) |
2 | | tbw-ax1 1708 |
. . . . . 6
⊢ ((𝜓 → ⊥) → ((⊥
→ 𝜒) → (𝜓 → 𝜒))) |
3 | | tbwlem1 1713 |
. . . . . 6
⊢ (((𝜓 → ⊥) → ((⊥
→ 𝜒) → (𝜓 → 𝜒))) → ((⊥ → 𝜒) → ((𝜓 → ⊥) → (𝜓 → 𝜒)))) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ ((⊥
→ 𝜒) → ((𝜓 → ⊥) → (𝜓 → 𝜒))) |
5 | 1, 4 | ax-mp 5 |
. . . 4
⊢ ((𝜓 → ⊥) → (𝜓 → 𝜒)) |
6 | | tbwlem1 1713 |
. . . 4
⊢ (((𝜓 → ⊥) → (𝜓 → 𝜒)) → (𝜓 → ((𝜓 → ⊥) → 𝜒))) |
7 | 5, 6 | ax-mp 5 |
. . 3
⊢ (𝜓 → ((𝜓 → ⊥) → 𝜒)) |
8 | | tbw-ax1 1708 |
. . 3
⊢ ((𝜑 → (𝜓 → ⊥)) → (((𝜓 → ⊥) → 𝜒) → (𝜑 → 𝜒))) |
9 | | tbw-ax1 1708 |
. . 3
⊢ ((𝜓 → ((𝜓 → ⊥) → 𝜒)) → ((((𝜓 → ⊥) → 𝜒) → (𝜑 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))) |
10 | 7, 8, 9 | mpsyl 68 |
. 2
⊢ ((𝜑 → (𝜓 → ⊥)) → (𝜓 → (𝜑 → 𝜒))) |
11 | | tbw-ax1 1708 |
. 2
⊢ ((𝜓 → (𝜑 → 𝜒)) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃))) |
12 | 10, 11 | tbwsyl 1712 |
1
⊢ ((𝜑 → (𝜓 → ⊥)) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃))) |