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  37670  tsim1  38331  tsna1  38345  ecinn0  38548  aks4d1p7  42347  aks6d1c5  42403  onsupmaxb  43491  ifpxorcor  43727  ifpnot23b  43733  ifpnot23c  43735  ifpnot23d  43736  iunrelexp0  43953  expandrex  44543  con5VD  45150  sineq0ALT  45187  nepnfltpnf  45597  nemnftgtmnft  45599  sge0gtfsumgt  46697  atbiffatnnb  47168  ichnreuop  47728  islininds2  48740  nnolog2flm1  48846  line2ylem  49007