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  2666  necon4ad  2673  necon4ai  2691  eueq2  3243  ifnot  3950  nbusgra  23808  wlkntrl  23930  eupath2  24070  cnfn1dd  29355  cnfn2dd  29356  stoweidlem39  30568  vk15.4j  32076  zfregs2VD  32420  vk15.4jVD  32493  con3ALTVD  32495  axfrege41  36544

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