Theorem notnotb 317

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  notbid  320  con2bi  355  con1bii  358  con2bii  359  iman  405  imor  864  anor  996  alex  1846  necon1abid  2995  necon4abid  2997  necon2abid  2999  necon2bbid  3000  necon1abii  3005  dfral2  3113  dfss6  3926  falseral0OLD  4469  difsnpss  4767  xpimasn  6171  2mpo0  7645  bropfvvvv  8071  zfregs2  9688  nqereu  10887  ssnn0fi  13998  swrdnnn0nd  14670  pfxnd0  14702  zeo4  16372  sumodd  16422  ncoprmlnprm  16763  numedglnl  29345  ballotlemfc0  34790  ballotlemfcc  34791  bnj1143  35085  bnj1304  35114  bnj1189  35304  bj-cbvaew  37116  wl-ifp-ncond2  37959  tsim1  38629  tsna1  38643  ecinn0  38852  aks4d1p7  42700  aks6d1c5  42756  onsupmaxb  43816  ifpxorcor  44052  ifpnot23b  44058  ifpnot23c  44060  ifpnot23d  44061  iunrelexp0  44278  expandrex  44868  con5VD  45475  sineq0ALT  45512  nepnfltpnf  45918  nemnftgtmnft  45920  sge0gtfsumgt  47017  atbiffatnnb  47506  ichnreuop  48078  islininds2  49106  nnolog2flm1  49212  line2ylem  49373