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 821) and in particular for decidable propositions (see notnotrdc 833). 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  832  con1dc  846  notnotbdc  862  imanst  878  eueq2dc  2899  ddifstab  3254  ifnotdc  3556  ismkvnex  7119  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  bj-nnsn  13614  bj-nndcALT  13639  bdnthALT  13717