Theorem notbii 323

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 322	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbi 233	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  sylnbi  333  xchnxbi  335  xchbinx  337  oplem1  1072  nic-axALT  1704  tbw-bijust  1728  rb-bijust  1779  19.43OLD  1913  cbvexvw  2067  hbn1fw  2077  hba1w  2079  exexw  2083  excom  2197  cbvrexf  3350  cbvrexcsf  3896  dfss4  4222  neq0f  4302  n0el  4319  ab0ALT  4337  abn0  4341  pssdifcom2  4451  difprsnss  4767  brdif  5164  otthne  5468  otiunsndisj  5503  difopab  5817  rexiunxp  5826  rexxpf  5833  dm0rn0  5914  rnep  5917  somin1  6133  cnvdif  6140  difxp  6161  xpdifcnvepel  6166  imadif  6620  brprcneu  6871  brprcneuALT  6872  dffv2  6976  ovima0  7589  porpss  7724  tfinds  7852  poxp  8120  xpord2pred  8137  xpord2indlem  8139  tz7.48lem  8424  brsdom  8967  brsdom2  9085  unfi  9151  fimax2g  9242  ordunifi  9246  dfsup2  9400  supgtoreq  9427  infcllem  9444  suc11reg  9584  rankxplim2  9848  rankxplim3  9849  alephval3  10090  kmlem4  10133  cflim2  10242  isfin4-2  10293  fin23lem25  10303  fin1a2lem5  10383  fin12  10392  axcclem  10436  zorng  10483  alephadd  10557  fpwwe2  10623  axpre-lttri  11145  dfinfre  12191  infrenegsup  12193  arch  12496  rpneg  13045  xmulcom  13287  xmulneg1  13290  xmulf  13293  xrinfmss2  13332  difreicc  13506  fzp1nel  13635  ssnn0fi  14017  fsuppmapnn0fiubex  14024  hashfun  14470  swrdccatin2  14762  s3iunsndisj  15001  incexc2  15888  lcmftp  16689  f1omvdco3  19514  psgnunilem4  19562  gsumcom3  20043  gsumxp2  20045  0ringnnzr  20623  mdetunilem7  22775  fctop  23161  cctop  23163  ntreq0  23234  ordtbas2  23348  cmpcld  23559  hausdiag  23802  fbun  23997  fbfinnfr  23998  opnfbas  23999  fbasrn  24041  filuni  24042  ufinffr  24086  alexsubALTlem2  24205  plyn0mulidp  26442  ellogdm  26804  nosepon  27829  noextenddif  27832  nomaxmo  27862  nosupinfsep  27896  nocvxminlem  27947  bdayfinbndlem1  28660  numedglnl  29494  usgredg2v  29577  clwwlknon1nloop  30450  avril1  30814  shne0i  31800  chnlei  31837  cvnbtwn2  32639  cvnbtwn3  32640  cvnbtwn4  32641  chrelat2i  32717  atabs2i  32754  dmdbr5ati  32774  nmo  32836  disjdifprg  32920  eliccelico  33122  elicoelioo  33123  xrdifh  33125  f1ocnt  33145  tosglblem  33294  xrnarchi  33504  elrgspnlem2  33563  fldextrspunlsplem  34063  hasheuni  34475  cntnevol  34618  sitgaddlemb  34738  eulerpartlemgs2  34770  ballotlem2  34879  ballotlemodife  34888  bnj1143  35178  bnj1304  35207  bnj1476  35235  bnj1533  35240  bnj1174  35391  bnj1204  35400  bnj1280  35408  nummin  35484  axreg  35540  axregscl  35541  noinfepregs  35546  axregs  35552  kardexen  35576  vonf1wev  35592  vonf1owevOLD  35594  0nn0m1nnn0  35604  lfuhgr3  35612  erdszelem9  35691  fmla0disjsuc  35890  dftr6  36243  fundmpss  36259  dfon2lem5  36277  dfon2lem8  36280  dfon2lem9  36281  wzel  36314  elfuns  36405  dfrecs2  36442  df3nandALT1  36930  andnand1  36932  imnand2  36933  regsfromregtco  37069  regsfromunir1  37071  bj-notalbii  37242  difunieq  38040  domalom  38070  fvineqsneq  38078  fdc  38416  nninfnub  38422  tsbi4  38805  ts3an2  38820  ts3an3  38821  ts3or1  38822  vvdifopab  38934  brvvdif  38937  n0elqs  39001  dfssr2  39248  lcvnbtwn2  39821  lcvnbtwn3  39822  cvrnbtwn3  40070  dalem18  40475  lhpocnel2  40813  cdleme0nex  41084  cdlemk19w  41766  dihglblem6  42134  dvh2dim  42239  dvh3dim3N  42243  aks4d1p7  42870  aks6d1c5  42926  sticksstones1  42933  aks6d1c6lem3  42959  redvmptabs  43141  ctbnfien  43565  rencldnfilem  43567  numinfctb  43850  onmaxnelsup  43970  onsupnmax  43975  onsupuni  43976  onsupeqnmax  43994  oenassex  44065  naddgeoa  44141  ifpnorcor  44226  ifpnancor  44227  ifpdfnan  44232  ifpananb  44252  ifpnannanb  44253  ifpxorxorb  44257  rp-isfinite6  44264  pwinfig  44307  elnonrel  44331  iunrelexp0  44448  frege131  44740  frege133  44742  compab  45171  zfregs2VD  45569  undif3VD  45610  sineq0ALT  45665  rext0  45667  permac8prim  45743  ndisj2  45791  ralfal  45899  uz0  46146  icccncfext  46621  itgioocnicc  46711  fourierdlem42  46883  fourierdlem62  46902  fourierdlem93  46933  fourierdlem101  46941  nsssmfmbf  47513  aiotavb  47847  afv2ndeffv0  48017  otiunsndisjX  48036  nltle2tri  48070  0nelsetpreimafv  48159  evennodd  48428