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

Theorem notnot 569
Description: Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds for all propositions, but its converse only holds for decidable propositions (see notnotrdc 762). (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 567 1  |-  ( ph  ->  -.  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 554  ax-in2 555
This theorem is referenced by:  notnotd  570  con3d  571  notnoti  584  pm3.24  637  notnotnot  638  biortn  674  dcn  757  con1dc  764  notnotbdc  777  eueq2dc  2737  difsnpssim  3535  xrlttri3  8819  nltpnft  8831  ngtmnft  8832  bdnthALT  10342
  Copyright terms: Public domain W3C validator