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

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  notbid  318  con2bi  353  con1bii  356  con2bii  357  iman  401  imor  852  anor  983  alex  1824  nfnbiOLD  1854  necon1abid  2985  necon4abid  2987  necon2abid  2989  necon2bbid  2990  necon1abii  2995  dfral2  3105  dfss6  3998  falseral0  4539  difsnpss  4832  xpimasn  6216  2mpo0  7699  bropfvvvv  8133  zfregs2  9802  nqereu  10998  ssnn0fi  14036  swrdnnn0nd  14704  pfxnd0  14736  zeo4  16386  sumodd  16436  ncoprmlnprm  16775  numedglnl  29179  ballotlemfc0  34457  ballotlemfcc  34458  bnj1143  34766  bnj1304  34795  bnj1189  34985  wl-ifp-ncond2  37431  tsim1  38090  tsna1  38104  ecinn0  38309  aks4d1p7  42040  aks6d1c5  42096  onsupmaxb  43200  ifpxorcor  43438  ifpnot23b  43444  ifpnot23c  43446  ifpnot23d  43447  iunrelexp0  43664  expandrex  44261  con5VD  44871  sineq0ALT  44908  nepnfltpnf  45257  nemnftgtmnft  45259  sge0gtfsumgt  46364  atbiffatnnb  46827  ichnreuop  47346  islininds2  48213  nnolog2flm1  48324  line2ylem  48485