Proof of Theorem stdcndcOLD
Step | Hyp | Ref
| Expression |
1 | | exmiddc 822 |
. . . . . 6
⊢
(DECID ¬ 𝜑 → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
2 | 1 | adantl 275 |
. . . . 5
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
3 | | df-stab 817 |
. . . . . . . 8
⊢
(STAB 𝜑
↔ (¬ ¬ 𝜑 →
𝜑)) |
4 | 3 | biimpi 119 |
. . . . . . 7
⊢
(STAB 𝜑
→ (¬ ¬ 𝜑 →
𝜑)) |
5 | 4 | orim2d 778 |
. . . . . 6
⊢
(STAB 𝜑
→ ((¬ 𝜑 ∨ ¬
¬ 𝜑) → (¬ 𝜑 ∨ 𝜑))) |
6 | 5 | adantr 274 |
. . . . 5
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) → ((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (¬ 𝜑 ∨ 𝜑))) |
7 | 2, 6 | mpd 13 |
. . . 4
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) → (¬ 𝜑 ∨ 𝜑)) |
8 | 7 | orcomd 719 |
. . 3
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) |
9 | | df-dc 821 |
. . 3
⊢
(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
10 | 8, 9 | sylibr 133 |
. 2
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) → DECID
𝜑) |
11 | | dcstab 830 |
. . 3
⊢
(DECID 𝜑 → STAB 𝜑) |
12 | | dcn 828 |
. . 3
⊢
(DECID 𝜑 → DECID ¬ 𝜑) |
13 | 11, 12 | jca 304 |
. 2
⊢
(DECID 𝜑 → (STAB 𝜑 ∧ DECID ¬ 𝜑)) |
14 | 10, 13 | impbii 125 |
1
⊢
((STAB 𝜑 ∧ DECID ¬ 𝜑) ↔ DECID
𝜑) |