This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \neg \neg φ \to φ$

Proof

Step	Hyp	Ref	Expression
1		pm2.18	$⊢ (\neg φ \to φ) \to φ$
2	1	jarli	$⊢ \neg \neg φ \to φ$