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

Proof of Theorem notnot1

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	con2i 120	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  notnoti  123  con1d  124  con4i  130  notnot  291  biortn  406  pm2.13  418  necon2ad  2670  necon4ad  2677  necon4ai  2695  eueq2  3273  ifnot  3986  nbusgra  24428  wlkntrl  24564  eupath2  24980  cnfn1dd  30492  cnfn2dd  30493  stoweidlem39  31821  vk15.4j  33298  zfregs2VD  33641  vk15.4jVD  33714  con3ALTVD  33716  axfrege41  37871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8