Theorem notnotr 132

Description: Double negation elimination. Converse of notnot 144 and one implication of notnotb 317. 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.18 128	. 2 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
2	1	jarli 126	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:  notnotrd  135  con2d  136  con3d  155  notnotb  317  ecase3ad  1031  necon1ad  3033  necon4bd  3036  eulercrct  28021  noetalem3  33219  notornotel1  35388  mpobi123f  35455  mptbi12f  35459  oexpreposd  39199  axfrege31  40199  clsk1independent  40416  con3ALT2  40884  zfregs2VD  41195  con3ALTVD  41270  notnotrALT2  41281  suplesup  41627