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  2977  ddifstab  3337  ifnotdc  3642  ismkvnex  7345  xrlttri3  10022  nltpnft  10039  ngtmnft  10042  bj-nnsn  16265  bj-nndcALT  16290  bdnthALT  16366