Theorem notnot 595

Description: Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds for all propositions, but its converse only holds for decidable propositions (see notnotrdc 790). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Assertion

Ref	Expression
notnot	⊢ (𝜑 → ¬ ¬ 𝜑)

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	con2i 593	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 580  ax-in2 581

This theorem is referenced by:  notnotd  596  con3d  597  notnoti  610  pm3.24  663  notnotnot  664  biortn  700  imanst  780  dcn  785  con1dc  792  notnotbdc  805  eueq2dc  2789  ddifstab  3133  xrlttri3  9328  nltpnft  9340  ngtmnft  9341  bdnthALT  11999