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  986  necon1ad  2811  necon4bd  2814  eulercrct  27102  noetalem3  31865  notornotel1  33897  mpt2bi123f  33971  mptbi12f  33975  axfrege31  38127  clsk1independent  38344  con3ALT2  38736  zfregs2VD  39076  con3ALTVD  39152  notnotrALT2  39163  suplesup  39555