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  854  anor  985  alex  1828  necon1abid  2971  necon4abid  2973  necon2abid  2975  necon2bbid  2976  necon1abii  2981  dfral2  3089  dfss6  3925  falseral0OLD  4470  difsnpss  4765  xpimasn  6151  2mpo0  7617  bropfvvvv  8044  zfregs2  9654  nqereu  10852  ssnn0fi  13920  swrdnnn0nd  14592  pfxnd0  14624  zeo4  16277  sumodd  16327  ncoprmlnprm  16667  numedglnl  29229  ballotlemfc0  34671  ballotlemfcc  34672  bnj1143  34966  bnj1304  34995  bnj1189  35185  bj-cbvaew  36887  wl-ifp-ncond2  37720  tsim1  38381  tsna1  38395  ecinn0  38604  aks4d1p7  42453  aks6d1c5  42509  onsupmaxb  43596  ifpxorcor  43832  ifpnot23b  43838  ifpnot23c  43840  ifpnot23d  43841  iunrelexp0  44058  expandrex  44648  con5VD  45255  sineq0ALT  45292  nepnfltpnf  45701  nemnftgtmnft  45703  sge0gtfsumgt  46801  atbiffatnnb  47272  ichnreuop  47832  islininds2  48844  nnolog2flm1  48950  line2ylem  49111