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

Theorem notnot 618
 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 816) and in particular for decidable propositions (see notnotrdc 828). See also notnotnot 623. (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 616 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 603  ax-in2 604 This theorem is referenced by:  notnotd  619  con3d  620  notnotnot  623  notnoti  634  jcn  641  pm3.24  682  biortn  734  dcn  827  const  837  con1dc  841  notnotbdc  857  imanst  873  eueq2dc  2852  ddifstab  3203  ismkvnex  7022  xrlttri3  9576  nltpnft  9590  ngtmnft  9593  bj-nnsn  12934  bj-nndcALT  12952  bdnthALT  13022
 Copyright terms: Public domain W3C validator