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  985  necon1ad  2808  necon4bd  2811  eulercrct  27082  noetalem3  31839  notornotel1  33868  mpt2bi123f  33942  mptbi12f  33946  axfrege31  37947  clsk1independent  38164  con3ALT2  38556  zfregs2VD  38896  con3ALTVD  38972  notnotrALT2  38983  suplesup  39368
  Copyright terms: Public domain W3C validator