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

Theorem notnotb 316
Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)
Assertion
Ref Expression
notnotb (𝜑 ↔ ¬ ¬ 𝜑)

Proof of Theorem notnotb
StepHypRef Expression
1 notnot 144 . 2 (𝜑 → ¬ ¬ 𝜑)
2 notnotr 132 . 2 (¬ ¬ 𝜑𝜑)
31, 2impbii 210 1 (𝜑 ↔ ¬ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  notbid  319  jcn  338  con2bi  355  con1bii  358  con2bii  359  iman  402  imor  847  anor  976  ifpn  1064  noranOLD  1518  nororOLD  1520  alex  1817  nfnbi  1846  necon1abid  3054  necon4abid  3056  necon2abid  3058  necon2bbid  3059  necon1abii  3064  dfral2  3237  ralnex2OLD  3261  ralnex3OLD  3263  dfss6  3956  falseral0  4457  difsnpss  4734  xpimasn  6036  2mpo0  7383  bropfvvvv  7778  zfregs2  9164  nqereu  10340  ssnn0fi  13343  swrdnnn0nd  14008  pfxnd0  14040  zeo4  15677  sumodd  15729  ncoprmlnprm  16058  numedglnl  26857  ballotlemfc0  31650  ballotlemfcc  31651  bnj1143  31962  bnj1304  31991  bnj1189  32179  tsim1  35291  tsna1  35305  ecinn0  35490  ifpxorcor  39722  ifpnot23b  39728  ifpnot23c  39730  ifpnot23d  39731  iunrelexp0  39927  expandrex  40508  con5VD  41114  sineq0ALT  41151  nepnfltpnf  41490  nemnftgtmnft  41492  sge0gtfsumgt  42606  atbiffatnnb  43029  ichnreuop  43481  islininds2  44437  nnolog2flm1  44548  line2ylem  44636
  Copyright terms: Public domain W3C validator