Theorem notbii 320

Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

Ref	Expression
notbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
notbii	⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		notbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		notbi 319	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbi 230	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  sylnbi  330  xchnxbi  332  xchbinx  334  oplem1  1057  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  19.43OLD  1885  cbvexvw  2039  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2168  cbvrexf  3333  cgsex4gOLD  3490  cbvrexcsf  3894  dfss4  4223  neq0f  4302  n0el  4318  ab0ALT  4335  abn0  4339  pssdifcom2  4445  difprsnss  4757  brdif  5153  otthne  5442  otiunsndisj  5476  difopab  5787  rexiunxp  5797  rexxpf  5804  dm0rn0  5881  rnep  5884  somin1  6098  cnvdif  6109  difxp  6130  imadif  6584  brprcneu  6832  brprcneuALT  6833  dffv2  6937  ovima0  7547  porpss  7682  tfinds  7812  poxp  8080  xpord2pred  8097  xpord2indlem  8099  tz7.48lem  8382  brsdom  8923  brsdom2  9041  unfi  9107  fimax2g  9198  ordunifi  9202  dfsup2  9359  supgtoreq  9386  infcllem  9403  suc11reg  9540  rankxplim2  9804  rankxplim3  9805  alephval3  10032  kmlem4  10076  cflim2  10185  isfin4-2  10236  fin23lem25  10246  fin1a2lem5  10326  fin12  10335  axcclem  10379  zorng  10426  alephadd  10500  fpwwe2  10566  axpre-lttri  11088  dfinfre  12135  infrenegsup  12137  arch  12410  rpneg  12951  xmulcom  13193  xmulneg1  13196  xmulf  13199  xrinfmss2  13238  difreicc  13412  fzp1nel  13539  ssnn0fi  13920  fsuppmapnn0fiubex  13927  hashfun  14372  swrdccatin2  14664  s3iunsndisj  14903  incexc2  15773  lcmftp  16575  f1omvdco3  19390  psgnunilem4  19438  gsumcom3  19919  gsumxp2  19921  0ringnnzr  20470  mdetunilem7  22574  fctop  22960  cctop  22962  ntreq0  23033  ordtbas2  23147  cmpcld  23358  hausdiag  23601  fbun  23796  fbfinnfr  23797  opnfbas  23798  fbasrn  23840  filuni  23841  ufinffr  23885  alexsubALTlem2  24004  ellogdm  26616  nosepon  27645  noextenddif  27648  nomaxmo  27678  nosupinfsep  27712  nocvxminlem  27762  bdayfinbndlem1  28475  numedglnl  29229  usgredg2v  29312  clwwlknon1nloop  30186  avril1  30550  shne0i  31536  chnlei  31573  cvnbtwn2  32375  cvnbtwn3  32376  cvnbtwn4  32377  chrelat2i  32453  atabs2i  32490  dmdbr5ati  32510  nmo  32576  disjdifprg  32662  eliccelico  32868  elicoelioo  32869  xrdifh  32871  f1ocnt  32891  tosglblem  33067  xrnarchi  33278  elrgspnlem2  33337  fldextrspunlsplem  33851  hasheuni  34263  cntnevol  34406  sitgaddlemb  34526  eulerpartlemgs2  34558  ballotlem2  34667  ballotlemodife  34676  plymulx0  34725  bnj1143  34966  bnj1304  34995  bnj1476  35023  bnj1533  35028  bnj1174  35179  bnj1204  35188  bnj1280  35196  nummin  35270  axreg  35305  axregscl  35306  noinfepregs  35311  axregs  35317  vonf1owev  35324  0nn0m1nnn0  35329  lfuhgr3  35336  erdszelem9  35415  fmla0disjsuc  35614  dftr6  35967  fundmpss  35983  dfon2lem5  36001  dfon2lem8  36004  dfon2lem9  36005  wzel  36038  elfuns  36129  dfrecs2  36166  df3nandALT1  36615  andnand1  36617  imnand2  36618  regsfromregtr  36690  regsfromunir1  36692  bj-notalbii  36852  difunieq  37629  domalom  37659  fvineqsneq  37667  fdc  37996  nninfnub  38002  tsbi4  38387  ts3an2  38402  ts3an3  38403  ts3or1  38404  vvdifopab  38516  brvvdif  38519  n0elqs  38583  dfssr2  38830  lcvnbtwn2  39403  lcvnbtwn3  39404  cvrnbtwn3  39652  dalem18  40057  lhpocnel2  40395  cdleme0nex  40666  cdlemk19w  41348  dihglblem6  41716  dvh2dim  41821  dvh3dim3N  41825  aks4d1p7  42453  aks6d1c5  42509  sticksstones1  42516  aks6d1c6lem3  42542  redvmptabs  42730  ctbnfien  43175  rencldnfilem  43177  numinfctb  43460  onmaxnelsup  43580  onsupnmax  43585  onsupuni  43586  onsupeqnmax  43604  oenassex  43675  naddgeoa  43751  ifpnorcor  43836  ifpnancor  43837  ifpdfnan  43842  ifpananb  43862  ifpnannanb  43863  ifpxorxorb  43867  rp-isfinite6  43874  pwinfig  43917  elnonrel  43941  iunrelexp0  44058  frege131  44350  frege133  44352  compab  44797  zfregs2VD  45196  undif3VD  45237  sineq0ALT  45292  rext0  45294  permac8prim  45370  ndisj2  45411  ralfal  45520  uz0  45770  icccncfext  46245  itgioocnicc  46335  fourierdlem42  46507  fourierdlem62  46526  fourierdlem93  46557  fourierdlem101  46565  nsssmfmbf  47137  aiotavb  47450  afv2ndeffv0  47620  otiunsndisjX  47639  nltle2tri  47673  0nelsetpreimafv  47750  evennodd  48003