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  853  anor  984  alex  1823  nfnbiOLD  1853  necon1abid  2977  necon4abid  2979  necon2abid  2981  necon2bbid  2982  necon1abii  2987  dfral2  3097  dfss6  3985  falseral0  4522  difsnpss  4812  xpimasn  6207  2mpo0  7682  bropfvvvv  8116  zfregs2  9771  nqereu  10967  ssnn0fi  14023  swrdnnn0nd  14691  pfxnd0  14723  zeo4  16372  sumodd  16422  ncoprmlnprm  16762  numedglnl  29176  ballotlemfc0  34474  ballotlemfcc  34475  bnj1143  34783  bnj1304  34812  bnj1189  35002  wl-ifp-ncond2  37448  tsim1  38117  tsna1  38131  ecinn0  38335  aks4d1p7  42065  aks6d1c5  42121  onsupmaxb  43228  ifpxorcor  43466  ifpnot23b  43472  ifpnot23c  43474  ifpnot23d  43475  iunrelexp0  43692  expandrex  44288  con5VD  44898  sineq0ALT  44935  nepnfltpnf  45292  nemnftgtmnft  45294  sge0gtfsumgt  46399  atbiffatnnb  46862  ichnreuop  47397  islininds2  48330  nnolog2flm1  48440  line2ylem  48601