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  1827  necon1abid  2968  necon4abid  2970  necon2abid  2972  necon2bbid  2973  necon1abii  2978  dfral2  3085  dfss6  3921  falseral0OLD  4466  difsnpss  4761  xpimasn  6141  2mpo0  7605  bropfvvvv  8032  zfregs2  9640  nqereu  10838  ssnn0fi  13906  swrdnnn0nd  14578  pfxnd0  14610  zeo4  16263  sumodd  16313  ncoprmlnprm  16653  numedglnl  29166  ballotlemfc0  34599  ballotlemfcc  34600  bnj1143  34895  bnj1304  34924  bnj1189  35114  wl-ifp-ncond2  37609  tsim1  38270  tsna1  38284  ecinn0  38485  aks4d1p7  42276  aks6d1c5  42332  onsupmaxb  43423  ifpxorcor  43659  ifpnot23b  43665  ifpnot23c  43667  ifpnot23d  43668  iunrelexp0  43885  expandrex  44475  con5VD  45082  sineq0ALT  45119  nepnfltpnf  45529  nemnftgtmnft  45531  sge0gtfsumgt  46629  atbiffatnnb  47100  ichnreuop  47660  islininds2  48672  nnolog2flm1  48778  line2ylem  48939