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  2979  necon4abid  2981  necon2abid  2983  necon2bbid  2984  necon1abii  2989  dfral2  3099  dfss6  3971  falseral0  4519  difsnpss  4810  xpimasn  6184  2mpo0  7657  bropfvvvv  8080  zfregs2  9730  nqereu  10926  ssnn0fi  13954  swrdnnn0nd  14610  pfxnd0  14642  zeo4  16285  sumodd  16335  ncoprmlnprm  16668  numedglnl  28659  ballotlemfc0  33777  ballotlemfcc  33778  bnj1143  34087  bnj1304  34116  bnj1189  34306  wl-ifp-ncond2  36649  tsim1  37301  tsna1  37315  ecinn0  37525  aks4d1p7  41254  onsupmaxb  42290  ifpxorcor  42529  ifpnot23b  42535  ifpnot23c  42537  ifpnot23d  42538  iunrelexp0  42755  expandrex  43353  con5VD  43963  sineq0ALT  44000  nepnfltpnf  44351  nemnftgtmnft  44353  sge0gtfsumgt  45458  atbiffatnnb  45921  ichnreuop  46439  islininds2  47253  nnolog2flm1  47364  line2ylem  47525