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