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 ⊢ (¬ ¬ 𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  notnotrd  134  con2d  135  con3d  153  notnotb  318  necon1ad  2973  necon4bd  2976  noetasuplem4  28093  eulercrct  30843  expgt0b  33408  notornotel1  39027  mpobi123f  39094  mptbi12f  39098  oexpreposd  43379  axfrege31  44832  clsk1independent  45045  con3ALT2  45512  zfregs2VD  45822  con3ALTVD  45897  notnotrALT2  45908  suplesup  46350