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, 5-Aug-1993.) (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  eueq2  3130  ifnot  3831  nbusgra  23274  wlkntrl  23396  eupath2  23536  cnfn1dd  28820  cnfn2dd  28821  stoweidlem39  29759  vk15.4j  31066  zfregs2VD  31411  vk15.4jVD  31484  con3ALTVD  31486
  Copyright terms: Public domain W3C validator