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

Theorem notnot 603
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 801) and in particular for decidable propositions (see notnotrdc 813). See also notnotnot 608. (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 601 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 588  ax-in2 589
This theorem is referenced by:  notnotd  604  con3d  605  notnotnot  608  notnoti  619  jcn  626  pm3.24  667  biortn  719  dcn  812  const  822  con1dc  826  notnotbdc  842  imanst  858  eueq2dc  2830  ddifstab  3178  ismkvnex  6997  xrlttri3  9551  nltpnft  9565  ngtmnft  9568  bj-nnsn  12872  bj-nndcALT  12890  bdnthALT  12960
  Copyright terms: Public domain W3C validator