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  3933  falseral0  4475  difsnpss  4767  xpimasn  6146  2mpo0  7618  bropfvvvv  8048  zfregs2  9662  nqereu  10858  ssnn0fi  13926  swrdnnn0nd  14597  pfxnd0  14629  zeo4  16284  sumodd  16334  ncoprmlnprm  16674  numedglnl  29124  ballotlemfc0  34477  ballotlemfcc  34478  bnj1143  34773  bnj1304  34802  bnj1189  34992  wl-ifp-ncond2  37446  tsim1  38117  tsna1  38131  ecinn0  38328  aks4d1p7  42064  aks6d1c5  42120  onsupmaxb  43221  ifpxorcor  43458  ifpnot23b  43464  ifpnot23c  43466  ifpnot23d  43467  iunrelexp0  43684  expandrex  44274  con5VD  44882  sineq0ALT  44919  nepnfltpnf  45331  nemnftgtmnft  45333  sge0gtfsumgt  46434  atbiffatnnb  46906  ichnreuop  47466  islininds2  48466  nnolog2flm1  48572  line2ylem  48733