Theorem notnot 619

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 817) and in particular for decidable propositions (see notnotrdc 829). See also notnotnot 624. (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 617	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 604  ax-in2 605

This theorem is referenced by:  notnotd  620  con3d  621  notnotnot  624  notnoti  635  pm3.24  683  biortn  735  dcn  828  const  838  con1dc  842  notnotbdc  858  imanst  874  eueq2dc  2881  ddifstab  3235  ismkvnex  7077  xrlttri3  9682  nltpnft  9696  ngtmnft  9699  bj-nnsn  13247  bj-nndcALT  13268  bdnthALT  13348