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  2970  necon4abid  2972  necon2abid  2974  necon2bbid  2975  necon1abii  2980  dfral2  3087  dfss6  3923  falseral0OLD  4468  difsnpss  4763  xpimasn  6143  2mpo0  7607  bropfvvvv  8034  zfregs2  9642  nqereu  10840  ssnn0fi  13908  swrdnnn0nd  14580  pfxnd0  14612  zeo4  16265  sumodd  16315  ncoprmlnprm  16655  numedglnl  29217  ballotlemfc0  34650  ballotlemfcc  34651  bnj1143  34946  bnj1304  34975  bnj1189  35165  wl-ifp-ncond2  37666  tsim1  38327  tsna1  38341  ecinn0  38542  aks4d1p7  42333  aks6d1c5  42389  onsupmaxb  43477  ifpxorcor  43713  ifpnot23b  43719  ifpnot23c  43721  ifpnot23d  43722  iunrelexp0  43939  expandrex  44529  con5VD  45136  sineq0ALT  45173  nepnfltpnf  45583  nemnftgtmnft  45585  sge0gtfsumgt  46683  atbiffatnnb  47154  ichnreuop  47714  islininds2  48726  nnolog2flm1  48832  line2ylem  48993