Theorem notnot 632

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 836) and in particular for decidable propositions (see notnotrdc 848). See also notnotnot 637. (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 630	1 ⊢ (𝜑 → ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  633  con3d  634  notnotnot  637  notnoti  648  pm3.24  698  biortn  750  dcn  847  con1dc  861  notnotbdc  877  imanst  893  eueq2dc  2976  ddifstab  3336  ifnotdc  3641  ismkvnex  7318  xrlttri3  9989  nltpnft  10006  ngtmnft  10009  bj-nnsn  16055  bj-nndcALT  16080  bdnthALT  16156