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  7496  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  bj-nnsn  16927  bj-nndcALT  16952  bdnthALT  17027  stnot  17205