Theorem notnot 630

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 833) and in particular for decidable propositions (see notnotrdc 845). See also notnotnot 635. (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 628	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  631  con3d  632  notnotnot  635  notnoti  646  pm3.24  695  biortn  747  dcn  844  con1dc  858  notnotbdc  874  imanst  890  eueq2dc  2950  ddifstab  3309  ifnotdc  3614  ismkvnex  7272  xrlttri3  9939  nltpnft  9956  ngtmnft  9959  bj-nnsn  15808  bj-nndcALT  15833  bdnthALT  15909