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

Theorem notnot 594
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 789). (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 592 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 579  ax-in2 580
This theorem is referenced by:  notnotd  595  con3d  596  notnoti  609  pm3.24  662  notnotnot  663  biortn  699  imanst  779  dcn  784  con1dc  791  notnotbdc  804  eueq2dc  2788  ddifstab  3132  xrlttri3  9265  nltpnft  9277  ngtmnft  9278  bdnthALT  11681
  Copyright terms: Public domain W3C validator