Proof of Theorem con3OLD
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ ((𝜓 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → (𝜓 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓))))) |
2 | 1 | notbid 308 |
. . 3
⊢ ((𝜓 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → (¬ 𝜓 ↔ ¬ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓))))) |
3 | 2 | imbi1d 331 |
. 2
⊢ ((𝜓 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → ((¬ 𝜓 → ¬ 𝜑) ↔ (¬ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓))) → ¬ 𝜑))) |
4 | 1 | imbi2d 330 |
. . . 4
⊢ ((𝜓 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → ((𝜑 → 𝜓) ↔ (𝜑 → ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))))) |
5 | | id 22 |
. . . . 5
⊢ ((𝜑 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → (𝜑 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓))))) |
6 | 5 | imbi2d 330 |
. . . 4
⊢ ((𝜑 ↔ ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) → ((𝜑 → 𝜑) ↔ (𝜑 → ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))))) |
7 | | id 22 |
. . . 4
⊢ (𝜑 → 𝜑) |
8 | 4, 6, 7 | elimhOLD 1033 |
. . 3
⊢ (𝜑 → ((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓)))) |
9 | 8 | con3i 150 |
. 2
⊢ (¬
((𝜓 ∧ (𝜑 → 𝜓)) ∨ (𝜑 ∧ ¬ (𝜑 → 𝜓))) → ¬ 𝜑) |
10 | 3, 9 | dedtOLD 1034 |
1
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) |