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

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

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  con2bi  354  con1bii  357  con2bii  358  iman  402  imor  859  anor  990  alex  1833  necon1abid  2972  necon4abid  2974  necon2abid  2976  necon2bbid  2977  necon1abii  2982  dfral2  3090  dfss6  3905  falseral0OLD  4443  difsnpss  4740  xpimasn  6136  2mpo0  7605  bropfvvvv  8031  zfregs2  9645  nqereu  10843  ssnn0fi  13938  swrdnnn0nd  14610  pfxnd0  14642  zeo4  16298  sumodd  16348  ncoprmlnprm  16689  numedglnl  29231  ballotlemfc0  34677  ballotlemfcc  34678  bnj1143  34972  bnj1304  35001  bnj1189  35191  bj-cbvaew  36984  wl-ifp-ncond2  37827  tsim1  38497  tsna1  38511  ecinn0  38720  aks4d1p7  42568  aks6d1c5  42624  onsupmaxb  43684  ifpxorcor  43920  ifpnot23b  43926  ifpnot23c  43928  ifpnot23d  43929  iunrelexp0  44146  expandrex  44736  con5VD  45343  sineq0ALT  45380  nepnfltpnf  45787  nemnftgtmnft  45789  sge0gtfsumgt  46886  atbiffatnnb  47375  ichnreuop  47947  islininds2  48975  nnolog2flm1  49081  line2ylem  49242