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  2911  ddifstab  3268  ifnotdc  3572  ismkvnex  7153  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  bj-nnsn  14488  bj-nndcALT  14513  bdnthALT  14590