Theorem notnotr 131

Description: Double negation elimination. Converse of notnot 143 and one implication of notnotb 318. 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 129	. 2 ⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
2	1	jarli 127	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  134  con2d  135  con3d  153  notnotb  318  necon1ad  2981  necon4bd  2984  noetasuplem4  27866  eulercrct  30534  expgt0b  33102  notornotel1  38634  mpobi123f  38701  mptbi12f  38705  oexpreposd  42973  axfrege31  44451  clsk1independent  44664  con3ALT2  45131  zfregs2VD  45441  con3ALTVD  45516  notnotrALT2  45527  suplesup  45947