Theorem notnot 634

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 838) and in particular for decidable propositions (see notnotrdc 850). See also notnotnot 639. (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 632	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  635  con3d  636  notnotnot  639  notnoti  650  pm3.24  700  biortn  752  dcn  849  con1dc  863  notnotbdc  879  imanst  895  eueq2dc  2979  ddifstab  3339  ifnotdc  3644  ismkvnex  7353  xrlttri3  10031  nltpnft  10048  ngtmnft  10051  bj-nnsn  16329  bj-nndcALT  16354  bdnthALT  16430