Proof of Theorem mercolem3
Step | Hyp | Ref
| Expression |
1 | | merco2 1743 |
. 2
⊢ (((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) |
2 | | merco2 1743 |
. . . 4
⊢ (((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓)) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))) |
3 | | mercolem2 1745 |
. . . . . . 7
⊢ (((𝜓 → (𝜑 → 𝜒)) → 𝜓) → ((⊥ → 𝜑) → ((⊥ → 𝜑) → 𝜓))) |
4 | | merco2 1743 |
. . . . . . 7
⊢ ((((𝜓 → (𝜑 → 𝜒)) → 𝜓) → ((⊥ → 𝜑) → ((⊥ → 𝜑) → 𝜓))) → ((((⊥ → 𝜑) → 𝜓) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))))) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢
((((⊥ → 𝜑)
→ 𝜓) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))))) |
6 | | merco2 1743 |
. . . . . 6
⊢
(((((⊥ → 𝜑)
→ 𝜓) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))))) → ((((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → 𝜓)) → ((⊥ → 𝜑) → ((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓))))) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ ((((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → 𝜓)) → ((⊥ → 𝜑) → ((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓)))) |
8 | | merco2 1743 |
. . . . 5
⊢
(((((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))) → ((⊥ → 𝜑) → 𝜓)) → ((⊥ → 𝜑) → ((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓)))) → ((((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓)) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))))))) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢ ((((𝜒 → 𝜑) → ((⊥ → 𝜑) → 𝜓)) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))))) |
10 | 2, 9 | ax-mp 5 |
. . 3
⊢ ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))))) |
11 | 1, 10 | ax-mp 5 |
. 2
⊢ ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))) |
12 | 1, 11 | ax-mp 5 |
1
⊢ ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒))) |