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

Theorem notnot 629
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 831) and in particular for decidable propositions (see notnotrdc 843). See also notnotnot 634. (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 627 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 614  ax-in2 615
This theorem is referenced by:  notnotd  630  con3d  631  notnotnot  634  notnoti  645  pm3.24  693  biortn  745  dcn  842  con1dc  856  notnotbdc  872  imanst  888  eueq2dc  2911  ddifstab  3268  ifnotdc  3572  ismkvnex  7153  xrlttri3  9797  nltpnft  9814  ngtmnft  9817  bj-nnsn  14488  bj-nndcALT  14513  bdnthALT  14590
  Copyright terms: Public domain W3C validator