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  2861  ddifstab  3213  ismkvnex  7037  xrlttri3  9613  nltpnft  9627  ngtmnft  9630  bj-nnsn  13116  bj-nndcALT  13134  bdnthALT  13204