MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnotb Structured version   Visualization version   GIF version

Theorem notnotb 302
Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)
Assertion
Ref Expression
notnotb (𝜑 ↔ ¬ ¬ 𝜑)

Proof of Theorem notnotb
StepHypRef Expression
1 notnot 134 . 2 (𝜑 → ¬ ¬ 𝜑)
2 notnotr 123 . 2 (¬ ¬ 𝜑𝜑)
31, 2impbii 197 1 (𝜑 ↔ ¬ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  notnotdOLD  303  notbid  306  con2bi  341  con1bii  344  imor  426  iman  438  dfbi3  932  ifpn  1015  alex  1742  necon1abid  2819  necon4abid  2821  necon2abid  2823  necon2bbid  2824  necon1abii  2829  dfral2  2976  ralnex2  3026  ralnex3  3027  elsymdifxor  3811  difsnpss  4278  xpimasn  5484  2mpt20  6757  bropfvvvv  7121  zfregs2  8469  nqereu  9607  ssnn0fi  12601  zeo4  14846  sumodd  14895  ncoprmlnprm  15220  wlkcpr  25823  vdn0frgrav2  26316  vdgn0frgrav2  26317  ballotlemfc0  29687  ballotlemfcc  29688  bnj1143  29921  bnj1304  29950  bnj1189  30137  bj-nfn  31601  wl-nfnbi  32289  tsim1  32903  tsna1  32917  ifpxorcor  36636  ifpnot23b  36642  ifpnot23c  36644  ifpnot23d  36645  iunrelexp0  36809  dfss6  36878  con5VD  37954  sineq0ALT  37991  jcn  38024  nepnfltpnf  38296  nemnftgtmnft  38298  sge0gtfsumgt  39133  atbiffatnnb  39525  falseral0  40106  islininds2  42062  nnolog2flm1  42177
  Copyright terms: Public domain W3C validator