---

Step * 1 1 of Lemma sq_stable__from_stable


1. P : ℙ
2. P supposing ¬¬P
3. ↓P
⊢ ¬¬P
BY
{ (BasicSquashHD 3 THEN UnhideSinceCompTrivialConcl) }

1
1. P : ℙ
2. P supposing ¬¬P
3. P
⊢ ¬¬P

2
.....wf..... 
1. P : ℙ
2. P supposing ¬¬P
3. P
⊢ ¬P ∈ ℙ

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  P  supposing  \mneg{}\mneg{}P
3.  \mdownarrow{}P
\mvdash{}  \mneg{}\mneg{}P


By

---

Latex:
(BasicSquashHD  3  THEN  UnhideSinceCompTrivialConcl)

---

Home Index