Theorem notnot 619

Description: Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. The converse need not hold. It holds exactly for stable propositions (by definition, see df-stab 817) and in particular for decidable propositions (see notnotrdc 829). See also notnotnot 624. (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 617	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  620  con3d  621  notnotnot  624  notnoti  635  pm3.24  683  biortn  735  dcn  828  const  838  con1dc  842  notnotbdc  858  imanst  874  eueq2dc  2885  ddifstab  3239  ismkvnex  7098  xrlttri3  9704  nltpnft  9718  ngtmnft  9721  bj-nnsn  13320  bj-nndcALT  13341  bdnthALT  13421