Description: Double negation elimination. Converse of notnot and one implication of
notnotb . Theorem *2.14 of WhiteheadRussell p. 102. This was the
fifth axiom of Frege, specifically Proposition 31 of Frege1879 p. 44.
In classical logic (our logic) this is always true. In intuitionistic
logic this is not always true, and formulas for which it is true are
called "stable". (Contributed by NM, 29-Dec-1992)(Proof shortened by David Harvey, 5-Sep-1999)(Proof shortened by Josh Purinton, 29-Dec-2000)