Theorem notnotr 125

Description: Double negation elimination. Converse of notnot 136 and one implication of notnotb 304. 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.21 120	. 2 ⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → 𝜑))
2	1	pm2.18d 124	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:  notnotriOLD  127  notnotrd  128  con2d  129  con3d  148  notnotb  304  ecase3ad  1005  necon1ad  2840  necon4bd  2843  eulercrct  27220  noetalem3  31990  notornotel1  34027  mpt2bi123f  34101  mptbi12f  34105  axfrege31  38444  clsk1independent  38661  con3ALT2  39053  zfregs2VD  39390  con3ALTVD  39466  notnotrALT2  39477  suplesup  39868