Proof of Theorem mercolem4
Step | Hyp | Ref
| Expression |
1 | | merco2 1744 |
. 2
⊢ (((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) |
2 | | merco2 1744 |
. . . 4
⊢ ((((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) |
3 | | merco2 1744 |
. . . . . . . . 9
⊢ (((𝜑 → 𝜑) → ((⊥ → 𝜑) → (𝜃 → 𝜒))) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) |
4 | | mercolem1 1745 |
. . . . . . . . 9
⊢ ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → (𝜃 → 𝜒))) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → (((⊥ → 𝜑) → (𝜃 → 𝜒)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢ (((⊥
→ 𝜑) → (𝜃 → 𝜒)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) |
6 | | mercolem1 1745 |
. . . . . . . 8
⊢
((((⊥ → 𝜑)
→ (𝜃 → 𝜒)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) → ((𝜃 → 𝜒) → ((⊥ → 𝜑) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))))) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ ((𝜃 → 𝜒) → ((⊥ → 𝜑) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))))) |
8 | | merco2 1744 |
. . . . . . 7
⊢ (((𝜃 → 𝜒) → ((⊥ → 𝜑) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))))) → ((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)))) |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
⊢ ((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃))) |
10 | | mercolem3 1747 |
. . . . . 6
⊢
(((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃))) → ((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → ((⊥ → 𝜑) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃))))) |
11 | 9, 10 | ax-mp 5 |
. . . . 5
⊢ ((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → ((⊥ → 𝜑) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)))) |
12 | | merco2 1744 |
. . . . 5
⊢
(((((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) → 𝜃) → ((⊥ → 𝜑) → (((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)))) → (((((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))))))) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢
(((((𝜂 → 𝜑) → 𝜑) → ((⊥ → 𝜑) → 𝜃)) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))))) |
14 | 2, 13 | ax-mp 5 |
. . 3
⊢ ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))))) |
15 | 1, 14 | ax-mp 5 |
. 2
⊢ ((((𝜑 → 𝜑) → ((⊥ → 𝜑) → 𝜑)) → ((𝜑 → 𝜑) → (𝜑 → (𝜑 → 𝜑)))) → ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))) |
16 | 1, 15 | ax-mp 5 |
1
⊢ ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑)))) |