Theorem notnot 618

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 816) and in particular for decidable propositions (see notnotrdc 828). See also notnotnot 623. (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 616	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 603  ax-in2 604

This theorem is referenced by:  notnotd  619  con3d  620  notnotnot  623  notnoti  634  pm3.24  682  biortn  734  dcn  827  const  837  con1dc  841  notnotbdc  857  imanst  873  eueq2dc  2857  ddifstab  3208  ismkvnex  7029  xrlttri3  9583  nltpnft  9597  ngtmnft  9600  bj-nnsn  12945  bj-nndcALT  12963  bdnthALT  13033