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

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( -. ph -> -. ph )
2	1	con2i 630	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 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  7322  xrlttri3  9993  nltpnft  10010  ngtmnft  10013  bj-nnsn  16097  bj-nndcALT  16122  bdnthALT  16198