Theorem notnotr 124

Description: Double negation elimination. Converse of notnot 135 and one implication of notnotb 303. 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.)

Assertion

Ref	Expression
notnotr	⊢ (¬ ¬ 𝜑 → 𝜑)

Proof of Theorem notnotr

Step	Hyp	Ref	Expression
1		pm2.21 119	. 2 ⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → 𝜑))
2	1	pm2.18d 123	1 ⊢ (¬ ¬ 𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  notnotriOLD  126  notnotrd  127  con2d  128  con3d  147  notnotb  303  ecase3ad  983  necon1ad  2799  necon4bd  2802  notornotel1  33067  mpt2bi123f  33141  mptbi12f  33145  axfrege31  37147  clsk1independent  37364  con3ALT2  37757  zfregs2VD  38098  con3ALTVD  38174  notnotrALT2  38185  suplesup  38496  eulercrct  41410