MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnot2 Structured version   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 
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 108 . 2  |-  ( -. 
-.  ph  ->  ( -. 
ph  ->  ph ) )
21pm2.18d 111 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  113  notnotri  114  con2d  115  con3d  133  notnot  291  ecase3ad  943  necon1ad  2683  necon4bd  2689  notornotel1  30413  mpt2bi123f  30490  mptbi12f  30494  con3ALT  32735  zfregs2VD  33077  con3ALTVD  33152  notnot2ALT2  33163  axfrege31  37200
  Copyright terms: Public domain W3C validator