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

Theorem notnotb 315
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  318  jcndOLD  337  con2bi  354  con1bii  357  con2bii  358  iman  403  imor  852  anor  982  ifpnOLD  1074  alex  1829  nfnbiOLD  1859  necon1abid  2981  necon4abid  2983  necon2abid  2985  necon2bbid  2986  necon1abii  2991  dfral2  3101  dfss6  3932  falseral0  4476  difsnpss  4766  xpimasn  6134  2mpo0  7593  bropfvvvv  8013  zfregs2  9603  nqereu  10799  ssnn0fi  13819  swrdnnn0nd  14476  pfxnd0  14508  zeo4  16155  sumodd  16205  ncoprmlnprm  16538  numedglnl  27881  ballotlemfc0  32853  ballotlemfcc  32854  bnj1143  33163  bnj1304  33192  bnj1189  33382  wl-ifp-ncond2  35822  tsim1  36475  tsna1  36489  ecinn0  36700  aks4d1p7  40426  ifpxorcor  41479  ifpnot23b  41485  ifpnot23c  41487  ifpnot23d  41488  iunrelexp0  41705  expandrex  42305  con5VD  42915  sineq0ALT  42952  nepnfltpnf  43302  nemnftgtmnft  43304  sge0gtfsumgt  44406  atbiffatnnb  44865  ichnreuop  45382  islininds2  46283  nnolog2flm1  46394  line2ylem  46555
  Copyright terms: Public domain W3C validator