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  403  imor  852  anor  982  ifpnOLD  1074  alex  1829  nfnbiOLD  1859  necon1abid  2980  necon4abid  2982  necon2abid  2984  necon2bbid  2985  necon1abii  2990  dfral2  3100  dfss6  3972  falseral0  4520  difsnpss  4811  xpimasn  6185  2mpo0  7655  bropfvvvv  8078  zfregs2  9728  nqereu  10924  ssnn0fi  13950  swrdnnn0nd  14606  pfxnd0  14638  zeo4  16281  sumodd  16331  ncoprmlnprm  16664  numedglnl  28404  ballotlemfc0  33491  ballotlemfcc  33492  bnj1143  33801  bnj1304  33830  bnj1189  34020  wl-ifp-ncond2  36346  tsim1  36998  tsna1  37012  ecinn0  37222  aks4d1p7  40948  onsupmaxb  41988  ifpxorcor  42227  ifpnot23b  42233  ifpnot23c  42235  ifpnot23d  42236  iunrelexp0  42453  expandrex  43051  con5VD  43661  sineq0ALT  43698  nepnfltpnf  44052  nemnftgtmnft  44054  sge0gtfsumgt  45159  atbiffatnnb  45622  ichnreuop  46140  islininds2  47165  nnolog2flm1  47276  line2ylem  47437