Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnot2 Unicode version

Theorem notnot2 112
 Description: Converse of double negation. 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; in intuitionistic logic, when this is true for some , then is 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
notnot2

Proof of Theorem notnot2
StepHypRef Expression
1 pm2.21 108 . 2
21pm2.18d 111 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4 This theorem is referenced by:  notnotrd  113  notnotri  114  con2d  115  con3d  133  notnot  291  ecase3ad  945  necon1ad  2673  necon4bd  2679  notornotel1  30495  mpt2bi123f  30571  mptbi12f  30575  con3ALT  33300  zfregs2VD  33641  con3ALTVD  33716  notnot2ALT2  33727  axfrege31  37860 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
 Copyright terms: Public domain W3C validator