MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnot Structured version   Visualization version   GIF version

Theorem notnot 134
Description: Double negation introduction. Converse of notnotr 123 and one implication of notnotb 302. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (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 22 . 2 𝜑 → ¬ 𝜑)
21con2i 132 1 (𝜑 → ¬ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  notnoti  135  notnotd  136  con1d  137  con4iOLD  143  notnotb  302  biortn  419  pm2.13  432  nfnt  1765  necon2ad  2792  necon4ad  2796  necon4ai  2808  eueq2  3342  ifnot  4078  nbusgra  25719  wlkntrl  25854  eupath2  26269  knoppndvlem10  31484  wl-orel12  32272  cnfn1dd  32863  cnfn2dd  32864  axfrege41  36957  vk15.4j  37554  zfregs2VD  37897  vk15.4jVD  37971  con3ALTVD  37973  stoweidlem39  38732
  Copyright terms: Public domain W3C validator