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

Theorem notnotb 306
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 138 . 2 (𝜑 → ¬ ¬ 𝜑)
2 notnotr 128 . 2 (¬ ¬ 𝜑𝜑)
31, 2impbii 200 1 (𝜑 ↔ ¬ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197
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 198
This theorem is referenced by:  notbid  309  con2bi  344  con1bii  347  iman  390  imor  879  ifpn  1095  alex  1920  nfnbi  1950  nfnbiOLD  1951  necon1abid  2975  necon4abid  2977  necon2abid  2979  necon2bbid  2980  necon1abii  2985  dfral2  3140  ralnex2  3192  ralnex3  3193  dfss6  3751  falseral0  4238  difsnpss  4492  xpimasn  5762  2mpt20  7080  bropfvvvv  7459  zfregs2  8824  nqereu  10004  ssnn0fi  12992  zeo4  15344  sumodd  15393  ncoprmlnprm  15715  numedglnl  26317  ballotlemfc0  31002  ballotlemfcc  31003  bnj1143  31309  bnj1304  31338  bnj1189  31525  wl-nfnbi  33739  tsim1  34358  tsna1  34372  ecinn0  34547  ifpxorcor  38497  ifpnot23b  38503  ifpnot23c  38505  ifpnot23d  38506  iunrelexp0  38669  con5VD  39788  sineq0ALT  39825  jcn  39857  nepnfltpnf  40196  nemnftgtmnft  40198  sge0gtfsumgt  41297  atbiffatnnb  41719  islininds2  42942  nnolog2flm1  43053
  Copyright terms: Public domain W3C validator