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 144	. 2 ⊢ (𝜑 → ¬ ¬ 𝜑)
2		notnotr 132	. 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  jcndOLD  339  con2bi  356  con1bii  359  con2bii  360  iman  404  imor  849  anor  979  ifpn  1068  noranOLD  1526  nororOLD  1528  alex  1825  nfnbi  1854  necon1abid  3053  necon4abid  3055  necon2abid  3057  necon2bbid  3058  necon1abii  3063  dfral2  3236  ralnex2OLD  3260  ralnex3OLD  3262  dfss6  3950  falseral0  4452  difsnpss  4733  xpimasn  6035  2mpo0  7387  bropfvvvv  7780  zfregs2  9168  nqereu  10344  ssnn0fi  13350  swrdnnn0nd  14013  pfxnd0  14045  zeo4  15682  sumodd  15734  ncoprmlnprm  16063  numedglnl  26927  ballotlemfc0  31771  ballotlemfcc  31772  bnj1143  32083  bnj1304  32112  bnj1189  32302  tsim1  35441  tsna1  35455  ecinn0  35640  ifpxorcor  39916  ifpnot23b  39922  ifpnot23c  39924  ifpnot23d  39925  iunrelexp0  40121  expandrex  40702  con5VD  41308  sineq0ALT  41345  nepnfltpnf  41684  nemnftgtmnft  41686  sge0gtfsumgt  42799  atbiffatnnb  43222  ichnreuop  43708  islininds2  44613  nnolog2flm1  44724  line2ylem  44812