Theorem notnotb 314

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  notbid  317  jcndOLD  336  con2bi  353  con1bii  356  con2bii  357  iman  402  imor  851  anor  981  ifpnOLD  1073  alex  1828  nfnbiOLD  1858  necon1abid  2978  necon4abid  2980  necon2abid  2982  necon2bbid  2983  necon1abii  2988  dfral2  3098  dfss6  3936  falseral0  4482  difsnpss  4772  xpimasn  6142  2mpo0  7607  bropfvvvv  8029  zfregs2  9678  nqereu  10874  ssnn0fi  13900  swrdnnn0nd  14556  pfxnd0  14588  zeo4  16231  sumodd  16281  ncoprmlnprm  16614  numedglnl  28158  ballotlemfc0  33181  ballotlemfcc  33182  bnj1143  33491  bnj1304  33520  bnj1189  33710  wl-ifp-ncond2  36009  tsim1  36662  tsna1  36676  ecinn0  36887  aks4d1p7  40613  onsupmaxb  41631  ifpxorcor  41870  ifpnot23b  41876  ifpnot23c  41878  ifpnot23d  41879  iunrelexp0  42096  expandrex  42694  con5VD  43304  sineq0ALT  43341  nepnfltpnf  43697  nemnftgtmnft  43699  sge0gtfsumgt  44804  atbiffatnnb  45267  ichnreuop  45784  islininds2  46685  nnolog2flm1  46796  line2ylem  46957