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  con2bi  353  con1bii  356  con2bii  357  iman  401  imor  852  anor  981  alex  1821  nfnbiOLD  1851  necon1abid  2975  necon4abid  2977  necon2abid  2979  necon2bbid  2980  necon1abii  2985  dfral2  3095  dfss6  3968  falseral0  4516  difsnpss  4807  xpimasn  6184  2mpo0  7665  bropfvvvv  8092  zfregs2  9751  nqereu  10947  ssnn0fi  13977  swrdnnn0nd  14633  pfxnd0  14665  zeo4  16309  sumodd  16359  ncoprmlnprm  16694  numedglnl  28951  ballotlemfc0  34107  ballotlemfcc  34108  bnj1143  34416  bnj1304  34445  bnj1189  34635  wl-ifp-ncond2  36939  tsim1  37598  tsna1  37612  ecinn0  37820  aks4d1p7  41549  aks6d1c5  41605  onsupmaxb  42658  ifpxorcor  42897  ifpnot23b  42903  ifpnot23c  42905  ifpnot23d  42906  iunrelexp0  43123  expandrex  43720  con5VD  44330  sineq0ALT  44367  nepnfltpnf  44715  nemnftgtmnft  44717  sge0gtfsumgt  45822  atbiffatnnb  46285  ichnreuop  46803  islininds2  47543  nnolog2flm1  47654  line2ylem  47815