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

Theorem notnot 619
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 817) and in particular for decidable propositions (see notnotrdc 829). See also notnotnot 624. (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 617 1 (𝜑 → ¬ ¬ 𝜑)
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 604  ax-in2 605
This theorem is referenced by:  notnotd  620  con3d  621  notnotnot  624  notnoti  635  pm3.24  683  biortn  735  dcn  828  const  838  con1dc  842  notnotbdc  858  imanst  874  eueq2dc  2885  ddifstab  3239  ismkvnex  7098  xrlttri3  9704  nltpnft  9718  ngtmnft  9721  bj-nnsn  13320  bj-nndcALT  13341  bdnthALT  13421
  Copyright terms: Public domain W3C validator