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 839) and in particular for decidable propositions (see notnotrdc 851). 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  701  biortn  753  dcn  850  con1dc  864  notnotbdc  880  imanst  896  eueq2dc  2980  ddifstab  3341  ifnotdc  3648  ismkvnex  7397  xrlttri3  10076  nltpnft  10093  ngtmnft  10096  bj-nnsn  16434  bj-nndcALT  16459  bdnthALT  16534