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 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  notbid  321  con2bi  356  con1bii  359  con2bii  360  iman  406  imor  866  anor  998  alex  1856  necon1abid  2996  necon4abid  2998  necon2abid  3000  necon2bbid  3001  necon1abii  3006  dfral2  3116  dfss6  3927  falseral0OLD  4476  difsnpss  4775  xpimasn  6183  2mpo0  7659  bropfvvvv  8083  zfregs2  9698  nqereu  10909  ssnn0fi  14017  swrdnnn0nd  14690  pfxnd0  14722  zeo4  16391  sumodd  16441  ncoprmlnprm  16782  numedglnl  29494  ballotlemfc0  34883  ballotlemfcc  34884  bnj1143  35178  bnj1304  35207  bnj1189  35397  bj-cbvaew  37286  wl-ifp-ncond2  38131  tsim1  38799  tsna1  38813  ecinn0  39022  aks4d1p7  42870  aks6d1c5  42926  onsupmaxb  43986  ifpxorcor  44222  ifpnot23b  44228  ifpnot23c  44230  ifpnot23d  44231  iunrelexp0  44448  expandrex  45022  con5VD  45628  sineq0ALT  45665  nepnfltpnf  46078  nemnftgtmnft  46080  sge0gtfsumgt  47177  atbiffatnnb  47669  ichnreuop  48241  islininds2  49284  nnolog2flm1  49390  line2ylem  49551