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

Step	Hyp	Ref	Expression
1		notnot 142	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 130	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 208	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

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  401  imor  849  anor  979  ifpnOLD  1071  noranOLD  1529  nororOLD  1531  alex  1829  nfnbiOLD  1859  necon1abid  2981  necon4abid  2983  necon2abid  2985  necon2bbid  2986  necon1abii  2991  dfral2  3164  dfss6  3906  falseral0  4447  difsnpss  4737  xpimasn  6077  2mpo0  7496  bropfvvvv  7903  zfregs2  9422  nqereu  10616  ssnn0fi  13633  swrdnnn0nd  14297  pfxnd0  14329  zeo4  15975  sumodd  16025  ncoprmlnprm  16360  numedglnl  27417  ballotlemfc0  32359  ballotlemfcc  32360  bnj1143  32670  bnj1304  32699  bnj1189  32889  wl-ifp-ncond2  35563  tsim1  36215  tsna1  36229  ecinn0  36412  aks4d1p7  40019  ifpxorcor  40981  ifpnot23b  40987  ifpnot23c  40989  ifpnot23d  40990  iunrelexp0  41199  expandrex  41799  con5VD  42409  sineq0ALT  42446  nepnfltpnf  42771  nemnftgtmnft  42773  sge0gtfsumgt  43871  atbiffatnnb  44294  ichnreuop  44812  islininds2  45713  nnolog2flm1  45824  line2ylem  45985