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

Theorem notnot 601
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 799) and in particular for decidable propositions (see notnotrdc 811). See also notnotnot 606. (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 599 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 586  ax-in2 587
This theorem is referenced by:  notnotd  602  con3d  603  notnotnot  606  notnoti  617  jcn  624  pm3.24  665  biortn  717  dcn  810  const  820  con1dc  824  notnotbdc  840  imanst  856  eueq2dc  2828  ddifstab  3176  ismkvnex  6995  xrlttri3  9523  nltpnft  9537  ngtmnft  9540  bj-nnsn  12756  bj-nndcALT  12774  bdnthALT  12844
  Copyright terms: Public domain W3C validator