ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  notnot Unicode version

Theorem notnot 629
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 831) and in particular for decidable propositions (see notnotrdc 843). See also notnotnot 634. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Assertion
Ref Expression
notnot  |-  ( ph  ->  -.  -.  ph )

Proof of Theorem notnot
StepHypRef Expression
1 id 19 . 2  |-  ( -. 
ph  ->  -.  ph )
21con2i 627 1  |-  ( ph  ->  -.  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 614  ax-in2 615
This theorem is referenced by:  notnotd  630  con3d  631  notnotnot  634  notnoti  645  pm3.24  693  biortn  745  dcn  842  con1dc  856  notnotbdc  872  imanst  888  eueq2dc  2910  ddifstab  3267  ifnotdc  3570  ismkvnex  7147  xrlttri3  9781  nltpnft  9798  ngtmnft  9801  bj-nnsn  14134  bj-nndcALT  14159  bdnthALT  14236
  Copyright terms: Public domain W3C validator