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

Theorem notnot 559
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 751). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Assertion
Ref Expression
notnot (𝜑 → ¬ ¬ 𝜑)

Proof of Theorem notnot
StepHypRef Expression
1 id 19 . 2 𝜑 → ¬ 𝜑)
21con2i 557 1 (𝜑 → ¬ ¬ 𝜑)
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 544  ax-in2 545
This theorem is referenced by:  notnotd  560  con3d  561  notnoti  574  pm3.24  627  notnotnot  628  biortn  664  dcn  746  con1dc  753  notnotbdc  766  eueq2dc  2711  difsnpssim  3504  xrlttri3  8685  nltpnft  8697  ngtmnft  8698  bdnthALT  9828
  Copyright terms: Public domain W3C validator