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  936  necon1ad  2665  necon4bd  2671  notornotel1  29041  mpt2bi123f  29118  mptbi12f  29122  con3ALT  31548  zfregs2VD  31890  con3ALTVD  31965  notnot2ALT2  31976
  Copyright terms: Public domain W3C validator