Theorem notnotb 318

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 143	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 131	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 212	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  con2bi  356  con1bii  359  con2bii  360  iman  407  imor  867  anor  998  alex  1859  necon1abid  2993  necon4abid  2995  necon2abid  2997  necon2bbid  2998  necon1abii  3003  dfral2  3113  dfss6  3921  falseral0OLD  4471  difsnpss  4770  xpimasn  6178  2mpo0  7664  bropfvvvv  8090  zfregs2  9715  nqereu  10941  ssnn0fi  14052  swrdnnn0nd  14729  pfxnd0  14761  zeo4  16431  sumodd  16481  ncoprmlnprm  16822  numedglnl  29604  ballotlemfc0  35007  ballotlemfcc  35008  bnj1143  35302  bnj1304  35331  bnj1189  35521  bj-cbvaew  37377  wl-ifp-ncond2  38222  tsim1  38881  tsna1  38895  ecinn0  39104  aks4d1p7  42952  aks6d1c5  43008  onsupmaxb  44083  ifpxorcor  44319  ifpnot23b  44325  ifpnot23c  44327  ifpnot23d  44328  iunrelexp0  44545  expandrex  45119  con5VD  45725  sineq0ALT  45762  nepnfltpnf  46175  nemnftgtmnft  46177  sge0gtfsumgt  47274  atbiffatnnb  47803  ichnreuop  48375  islininds2  49417  nnolog2flm1  49523  line2ylem  49684