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	|- ( ph -> -. -. ph )

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( -. ph -> -. ph )
2	1	con2i 627	1 |- ( ph -> -. -. ph )

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  7152  xrlttri3  9796  nltpnft  9813  ngtmnft  9816  bj-nnsn  14455  bj-nndcALT  14480  bdnthALT  14557