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

Theorem notnot2 116
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 
ph, then  ph 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  |-  ( -. 
-.  ph  ->  ph )

Proof of Theorem notnot2
StepHypRef Expression
1 pm2.21 112 . 2  |-  ( -. 
-.  ph  ->  ( -. 
ph  ->  ph ) )
21pm2.18d 115 1  |-  ( -. 
-.  ph  ->  ph )
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:  notnotrd  117  notnotri  118  con2d  119  con3d  139  notnot  293  ecase3ad  954  necon1ad  2641  necon4bd  2647  notornotel1  32251  mpt2bi123f  32326  mptbi12f  32330  axfrege31  36293  con3ALT  36751  zfregs2VD  37104  con3ALTVD  37180  notnot2ALT2  37191  suplesup  37410  nnfoctbdjlem  38078
  Copyright terms: Public domain W3C validator