Theorem notnot 638

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 843) and in particular for decidable propositions (see notnotrdc 855). See also notnotnot 643. (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 636	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  notnotd  639  con3d  640  notnotnot  643  notnoti  654  pm3.24  705  biortn  757  dcn  854  con1dc  868  notnotbdc  884  imanst  900  eueq2dc  2999  ddifstab  3361  ifnotdc  3679  ismkvnex  7495  xrlttri3  10199  nltpnft  10216  ngtmnft  10219  bj-nnsn  16761  bj-nndcALT  16786  bdnthALT  16861  stnot  17039