Theorem notnotr 130

Description: Double negation elimination. Converse of notnot 142 and one implication of notnotb 314. 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  133  con2d  134  con3d  152  notnotb  314  ecase3adOLD  1033  necon1ad  2959  necon4bd  2962  eulercrct  28507  noetasuplem4  33866  notornotel1  36180  mpobi123f  36247  mptbi12f  36251  oexpreposd  40242  axfrege31  41330  clsk1independent  41545  con3ALT2  42039  zfregs2VD  42350  con3ALTVD  42425  notnotrALT2  42436  suplesup  42768