Theorem notnot 624

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 826) and in particular for decidable propositions (see notnotrdc 838). See also notnotnot 629. (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 622	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 609  ax-in2 610

This theorem is referenced by:  notnotd  625  con3d  626  notnotnot  629  notnoti  640  pm3.24  688  biortn  740  dcn  837  con1dc  851  notnotbdc  867  imanst  883  eueq2dc  2903  ddifstab  3259  ifnotdc  3562  ismkvnex  7131  xrlttri3  9754  nltpnft  9771  ngtmnft  9774  bj-nnsn  13768  bj-nndcALT  13793  bdnthALT  13870