Theorem notnot 618

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 816) and in particular for decidable propositions (see notnotrdc 828). See also notnotnot 623. (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 616	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  619  con3d  620  notnotnot  623  notnoti  634  jcn  641  pm3.24  682  biortn  734  dcn  827  const  837  con1dc  841  notnotbdc  857  imanst  873  eueq2dc  2852  ddifstab  3203  ismkvnex  7022  xrlttri3  9576  nltpnft  9590  ngtmnft  9593  bj-nnsn  12934  bj-nndcALT  12952  bdnthALT  13022