---

Step * of Lemma double_neg_elim

(P:. (P  (P)))  (P:. ((P)  (P)))
BY
{ (Auto THEN InstHyp [P] 1 THEN Auto THEN D (-1) THEN Auto THEN D (-2)) }

1
1. P:. (P  (P))@i'
2. P : @i'
3. P
 P


(\mforall{}P:\mBbbP{}.  (\mdownarrow{}P  \mvee{}  (\mneg{}P)))  {}\mRightarrow{}  (\mforall{}P:\mBbbP{}.  ((\mneg{}\mneg{}\mdownarrow{}P)  {}\mRightarrow{}  (\mdownarrow{}P)))


By

(Auto  THEN  InstHyp  [\mkleeneopen{}P\mkleeneclose{}]  1\mcdot{}  THEN  Auto  THEN  D  (-1)  THEN  Auto  THEN  D  (-2))



Home Index