Metamath Proof Explorer


Theorem notnotr

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)

Ref Expression
Assertion notnotr ( ¬ ¬ 𝜑𝜑 )

Proof

Step Hyp Ref Expression
1 pm2.18 ( ( ¬ 𝜑𝜑 ) → 𝜑 )
2 1 jarli ( ¬ ¬ 𝜑𝜑 )