Theorem notnot 634

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 839) and in particular for decidable propositions (see notnotrdc 851). See also notnotnot 639. (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 632	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 619  ax-in2 620

This theorem is referenced by:  notnotd  635  con3d  636  notnotnot  639  notnoti  650  pm3.24  701  biortn  753  dcn  850  con1dc  864  notnotbdc  880  imanst  896  eueq2dc  2980  ddifstab  3341  ifnotdc  3648  ismkvnex  7414  xrlttri3  10093  nltpnft  10110  ngtmnft  10113  bj-nnsn  16451  bj-nndcALT  16476  bdnthALT  16551