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  1826  necon1abid  2963  necon4abid  2965  necon2abid  2967  necon2bbid  2968  necon1abii  2973  dfral2  3081  dfss6  3936  falseral0  4479  difsnpss  4771  xpimasn  6158  2mpo0  7638  bropfvvvv  8071  zfregs2  9686  nqereu  10882  ssnn0fi  13950  swrdnnn0nd  14621  pfxnd0  14653  zeo4  16308  sumodd  16358  ncoprmlnprm  16698  numedglnl  29071  ballotlemfc0  34484  ballotlemfcc  34485  bnj1143  34780  bnj1304  34809  bnj1189  34999  wl-ifp-ncond2  37453  tsim1  38124  tsna1  38138  ecinn0  38335  aks4d1p7  42071  aks6d1c5  42127  onsupmaxb  43228  ifpxorcor  43465  ifpnot23b  43471  ifpnot23c  43473  ifpnot23d  43474  iunrelexp0  43691  expandrex  44281  con5VD  44889  sineq0ALT  44926  nepnfltpnf  45338  nemnftgtmnft  45340  sge0gtfsumgt  46441  atbiffatnnb  46913  ichnreuop  47473  islininds2  48473  nnolog2flm1  48579  line2ylem  48740