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

Theorem notnot2 114
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 110 . 2  |-  ( -. 
-.  ph  ->  ( -. 
ph  ->  ph ) )
21pm2.18d 113 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  115  notnotri  116  con2d  117  con3d  135  notnot  291  ecase3ad  948  necon1ad  2621  necon4bd  2627  notornotel1  31790  mpt2bi123f  31866  mptbi12f  31870  axfrege31  35827  con3ALT  36330  zfregs2VD  36684  con3ALTVD  36760  notnot2ALT2  36771
  Copyright terms: Public domain W3C validator