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

Theorem notnot1 122
Description: Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Assertion
Ref Expression
notnot1  |-  ( ph  ->  -.  -.  ph )

Proof of Theorem notnot1
StepHypRef Expression
1 id 22 . 2  |-  ( -. 
ph  ->  -.  ph )
21con2i 120 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:  notnoti  123  con1d  124  con4i  130  notnot  291  biortn  406  pm2.13  418  necon2ad  2675  necon4ad  2682  necon4ai  2700  eueq2  3272  ifnot  3979  nbusgra  24092  wlkntrl  24228  eupath2  24644  cnfn1dd  30084  cnfn2dd  30085  stoweidlem39  31296  vk15.4j  32254  zfregs2VD  32598  vk15.4jVD  32671  con3ALTVD  32673  axfrege41  36732
  Copyright terms: Public domain W3C validator