Theorem notnotb 315

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  318  jcndOLD  337  con2bi  354  con1bii  357  con2bii  358  iman  402  imor  850  anor  980  ifpnOLD  1072  alex  1828  nfnbiOLD  1858  necon1abid  2982  necon4abid  2984  necon2abid  2986  necon2bbid  2987  necon1abii  2992  dfral2  3168  dfss6  3910  falseral0  4450  difsnpss  4740  xpimasn  6088  2mpo0  7518  bropfvvvv  7932  zfregs2  9491  nqereu  10685  ssnn0fi  13705  swrdnnn0nd  14369  pfxnd0  14401  zeo4  16047  sumodd  16097  ncoprmlnprm  16432  numedglnl  27514  ballotlemfc0  32459  ballotlemfcc  32460  bnj1143  32770  bnj1304  32799  bnj1189  32989  wl-ifp-ncond2  35636  tsim1  36288  tsna1  36302  ecinn0  36485  aks4d1p7  40091  ifpxorcor  41083  ifpnot23b  41089  ifpnot23c  41091  ifpnot23d  41092  iunrelexp0  41310  expandrex  41910  con5VD  42520  sineq0ALT  42557  nepnfltpnf  42881  nemnftgtmnft  42883  sge0gtfsumgt  43981  atbiffatnnb  44407  ichnreuop  44924  islininds2  45825  nnolog2flm1  45936  line2ylem  46097