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  2990  ddifstab  3351  ifnotdc  3661  ismkvnex  7446  xrlttri3  10130  nltpnft  10147  ngtmnft  10150  bj-nnsn  16505  bj-nndcALT  16530  bdnthALT  16605