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

Theorem notnot 592
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 785). (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 590 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 577  ax-in2 578
This theorem is referenced by:  notnotd  593  con3d  594  notnoti  607  pm3.24  660  notnotnot  661  biortn  697  dcn  780  con1dc  787  notnotbdc  800  eueq2dc  2776  ddifstab  3116  xrlttri3  9161  nltpnft  9173  ngtmnft  9174  bdnthALT  11068
  Copyright terms: Public domain W3C validator