Theorem notnot 629

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotd  630  con3d  631  notnotnot  634  notnoti  645  pm3.24  693  biortn  745  dcn  842  con1dc  856  notnotbdc  872  imanst  888  eueq2dc  2910  ddifstab  3267  ifnotdc  3571  ismkvnex  7150  xrlttri3  9793  nltpnft  9810  ngtmnft  9813  bj-nnsn  14345  bj-nndcALT  14370  bdnthALT  14447