Theorem notnotb 317

Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)

Assertion

Ref	Expression
notnotb	⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Proof of Theorem notnotb

Step	Hyp	Ref	Expression
1		notnot 144	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 132	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 211	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  notbid  320  jcndOLD  339  con2bi  356  con1bii  359  con2bii  360  iman  404  imor  849  anor  979  ifpn  1067  noranOLD  1521  nororOLD  1523  alex  1820  nfnbi  1849  necon1abid  3052  necon4abid  3054  necon2abid  3056  necon2bbid  3057  necon1abii  3062  dfral2  3235  ralnex2OLD  3259  ralnex3OLD  3261  dfss6  3955  falseral0  4457  difsnpss  4732  xpimasn  6035  2mpo0  7386  bropfvvvv  7779  zfregs2  9167  nqereu  10343  ssnn0fi  13345  swrdnnn0nd  14010  pfxnd0  14042  zeo4  15679  sumodd  15731  ncoprmlnprm  16060  numedglnl  26921  ballotlemfc0  31743  ballotlemfcc  31744  bnj1143  32055  bnj1304  32084  bnj1189  32274  tsim1  35400  tsna1  35414  ecinn0  35599  ifpxorcor  39832  ifpnot23b  39838  ifpnot23c  39840  ifpnot23d  39841  iunrelexp0  40037  expandrex  40618  con5VD  41224  sineq0ALT  41261  nepnfltpnf  41599  nemnftgtmnft  41601  sge0gtfsumgt  42715  atbiffatnnb  43138  ichnreuop  43624  islininds2  44529  nnolog2flm1  44640  line2ylem  44728