Theorem notnotb 316

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 144	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 132	. 2 ⊢ (¬ ¬ 𝜑 → 𝜑)
3	1, 2	impbii 210	1 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  notbid  319  jcn  338  con2bi  355  con1bii  358  con2bii  359  iman  402  imor  848  anor  977  ifpn  1065  noranOLD  1519  nororOLD  1521  alex  1811  nfnbi  1840  necon1abid  3024  necon4abid  3026  necon2abid  3028  necon2bbid  3029  necon1abii  3034  dfral2  3203  ralnex2OLD  3227  ralnex3OLD  3229  dfss6  3885  falseral0  4379  difsnpss  4653  xpimasn  5925  2mpo0  7259  bropfvvvv  7650  zfregs2  9028  nqereu  10204  ssnn0fi  13207  swrdnnn0nd  13858  pfxnd0  13890  zeo4  15524  sumodd  15576  ncoprmlnprm  15901  numedglnl  26616  ballotlemfc0  31363  ballotlemfcc  31364  bnj1143  31675  bnj1304  31704  bnj1189  31891  tsim1  34961  tsna1  34975  ecinn0  35160  ifpxorcor  39348  ifpnot23b  39354  ifpnot23c  39356  ifpnot23d  39357  iunrelexp0  39553  expandrex  40146  con5VD  40794  sineq0ALT  40831  nepnfltpnf  41172  nemnftgtmnft  41174  sge0gtfsumgt  42289  atbiffatnnb  42711  ichnreuop  43138  islininds2  44041  nnolog2flm1  44153  line2ylem  44241