MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnotr Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm2.21 120 . 2 (¬ ¬ 𝜑 → (¬ 𝜑𝜑))
21pm2.18d 124 1 (¬ ¬ 𝜑𝜑)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator