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

Theorem notnotb 314
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 142 . 2 (𝜑 → ¬ ¬ 𝜑)
2 notnotr 130 . 2 (¬ ¬ 𝜑𝜑)
31, 2impbii 208 1 (𝜑 ↔ ¬ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  notbid  317  jcndOLD  336  con2bi  353  con1bii  356  con2bii  357  iman  402  imor  851  anor  981  ifpnOLD  1073  alex  1828  nfnbiOLD  1858  necon1abid  2980  necon4abid  2982  necon2abid  2984  necon2bbid  2985  necon1abii  2990  dfral2  3100  dfss6  3931  falseral0  4475  difsnpss  4765  xpimasn  6133  2mpo0  7592  bropfvvvv  8012  zfregs2  9602  nqereu  10798  ssnn0fi  13818  swrdnnn0nd  14475  pfxnd0  14507  zeo4  16154  sumodd  16204  ncoprmlnprm  16537  numedglnl  27893  ballotlemfc0  32865  ballotlemfcc  32866  bnj1143  33175  bnj1304  33204  bnj1189  33394  wl-ifp-ncond2  35831  tsim1  36484  tsna1  36498  ecinn0  36709  aks4d1p7  40435  ifpxorcor  41510  ifpnot23b  41516  ifpnot23c  41518  ifpnot23d  41519  iunrelexp0  41736  expandrex  42336  con5VD  42946  sineq0ALT  42983  nepnfltpnf  43333  nemnftgtmnft  43335  sge0gtfsumgt  44437  atbiffatnnb  44896  ichnreuop  45413  islininds2  46314  nnolog2flm1  46425  line2ylem  46586
  Copyright terms: Public domain W3C validator