Theorem notnot 638

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 843) and in particular for decidable propositions (see notnotrdc 855). See also notnotnot 643. (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 636	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 623  ax-in2 624

This theorem is referenced by:  notnotd  639  con3d  640  notnotnot  643  notnoti  654  pm3.24  705  biortn  757  dcn  854  con1dc  868  notnotbdc  884  imanst  900  eueq2dc  2999  ddifstab  3361  ifnotdc  3676  ismkvnex  7485  xrlttri3  10178  nltpnft  10195  ngtmnft  10198  bj-nnsn  16675  bj-nndcALT  16700  bdnthALT  16775