Theorem notnotb 318

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 143	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 131	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 212	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbid  321  con2bi  356  con1bii  359  con2bii  360  iman  407  imor  867  anor  998  alex  1859  necon1abid  2994  necon4abid  2996  necon2abid  2998  necon2bbid  2999  necon1abii  3004  dfral2  3114  dfss6  3921  falseral0OLD  4471  difsnpss  4770  xpimasn  6177  2mpo0  7670  bropfvvvv  8103  zfregs2  9734  nqereu  11014  ssnn0fi  14128  swrdnnn0nd  14806  pfxnd0  14838  zeo4  16508  sumodd  16558  ncoprmlnprm  16904  numedglnl  29722  ballotlemfc0  35125  ballotlemfcc  35126  bnj1143  35420  bnj1304  35449  bnj1189  35639  bj-cbvaew  37543  wl-ifp-ncond2  38388  tsim1  39062  tsna1  39076  ecinn0  39285  aks4d1p7  43133  aks6d1c5  43189  onsupmaxb  44240  ifpxorcor  44476  ifpnot23b  44482  ifpnot23c  44484  ifpnot23d  44485  iunrelexp0  44701  expandrex  45275  con5VD  45881  sineq0ALT  45918  nepnfltpnf  46353  nemnftgtmnft  46355  sge0gtfsumgt  47452  atbiffatnnb  47981  ichnreuop  48553  islininds2  49595  nnolog2flm1  49701  line2ylem  49862