Theorem notnotr 130

Description: Double negation elimination. Converse of notnot 142 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  133  con2d  134  con3d  152  notnotb  317  necon1ad  2974  necon4bd  2977  noetasuplem4  27800  eulercrct  30444  expgt0b  33019  notornotel1  38594  mpobi123f  38661  mptbi12f  38665  oexpreposd  42931  axfrege31  44409  clsk1independent  44622  con3ALT2  45106  zfregs2VD  45416  con3ALTVD  45491  notnotrALT2  45502  suplesup  45915