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  3324  cbvrexcsf  3881  dfss4  4210  neq0f  4289  n0el  4305  ab0ALT  4322  abn0  4326  pssdifcom2  4431  difprsnss  4743  brdif  5139  otthne  5435  otiunsndisj  5469  difopab  5780  rexiunxp  5790  rexxpf  5797  dm0rn0  5874  rnep  5877  somin1  6091  cnvdif  6102  difxp  6123  imadif  6577  brprcneu  6825  brprcneuALT  6826  dffv2  6930  ovima0  7540  porpss  7675  tfinds  7805  poxp  8072  xpord2pred  8089  xpord2indlem  8091  tz7.48lem  8374  brsdom  8915  brsdom2  9033  unfi  9099  fimax2g  9190  ordunifi  9194  dfsup2  9351  supgtoreq  9378  infcllem  9395  suc11reg  9534  rankxplim2  9798  rankxplim3  9799  alephval3  10026  kmlem4  10070  cflim2  10179  isfin4-2  10230  fin23lem25  10240  fin1a2lem5  10320  fin12  10329  axcclem  10373  zorng  10420  alephadd  10494  fpwwe2  10560  axpre-lttri  11082  dfinfre  12131  infrenegsup  12133  arch  12428  rpneg  12970  xmulcom  13212  xmulneg1  13215  xmulf  13218  xrinfmss2  13257  difreicc  13431  fzp1nel  13559  ssnn0fi  13941  fsuppmapnn0fiubex  13948  hashfun  14393  swrdccatin2  14685  s3iunsndisj  14924  incexc2  15797  lcmftp  16599  f1omvdco3  19418  psgnunilem4  19466  gsumcom3  19947  gsumxp2  19949  0ringnnzr  20496  mdetunilem7  22596  fctop  22982  cctop  22984  ntreq0  23055  ordtbas2  23169  cmpcld  23380  hausdiag  23623  fbun  23818  fbfinnfr  23819  opnfbas  23820  fbasrn  23862  filuni  23863  ufinffr  23907  alexsubALTlem2  24026  ellogdm  26619  nosepon  27646  noextenddif  27649  nomaxmo  27679  nosupinfsep  27713  nocvxminlem  27763  bdayfinbndlem1  28476  numedglnl  29230  usgredg2v  29313  clwwlknon1nloop  30187  avril1  30551  shne0i  31537  chnlei  31574  cvnbtwn2  32376  cvnbtwn3  32377  cvnbtwn4  32378  chrelat2i  32454  atabs2i  32491  dmdbr5ati  32511  nmo  32577  disjdifprg  32663  eliccelico  32868  elicoelioo  32869  xrdifh  32871  f1ocnt  32891  tosglblem  33052  xrnarchi  33263  elrgspnlem2  33322  fldextrspunlsplem  33836  hasheuni  34248  cntnevol  34391  sitgaddlemb  34511  eulerpartlemgs2  34543  ballotlem2  34652  ballotlemodife  34661  plymulx0  34710  bnj1143  34951  bnj1304  34980  bnj1476  35008  bnj1533  35013  bnj1174  35164  bnj1204  35173  bnj1280  35181  nummin  35255  axreg  35290  axregscl  35291  noinfepregs  35296  axregs  35302  vonf1owev  35309  0nn0m1nnn0  35314  lfuhgr3  35321  erdszelem9  35400  fmla0disjsuc  35599  dftr6  35952  fundmpss  35968  dfon2lem5  35986  dfon2lem8  35989  dfon2lem9  35990  wzel  36023  elfuns  36114  dfrecs2  36151  df3nandALT1  36600  andnand1  36602  imnand2  36603  regsfromregtco  36739  regsfromunir1  36741  bj-notalbii  36913  difunieq  37707  domalom  37737  fvineqsneq  37745  fdc  38083  nninfnub  38089  tsbi4  38474  ts3an2  38489  ts3an3  38490  ts3or1  38491  vvdifopab  38603  brvvdif  38606  n0elqs  38670  dfssr2  38917  lcvnbtwn2  39490  lcvnbtwn3  39491  cvrnbtwn3  39739  dalem18  40144  lhpocnel2  40482  cdleme0nex  40753  cdlemk19w  41435  dihglblem6  41803  dvh2dim  41908  dvh3dim3N  41912  aks4d1p7  42539  aks6d1c5  42595  sticksstones1  42602  aks6d1c6lem3  42628  redvmptabs  42809  ctbnfien  43267  rencldnfilem  43269  numinfctb  43552  onmaxnelsup  43672  onsupnmax  43677  onsupuni  43678  onsupeqnmax  43696  oenassex  43767  naddgeoa  43843  ifpnorcor  43928  ifpnancor  43929  ifpdfnan  43934  ifpananb  43954  ifpnannanb  43955  ifpxorxorb  43959  rp-isfinite6  43966  pwinfig  44009  elnonrel  44033  iunrelexp0  44150  frege131  44442  frege133  44444  compab  44889  zfregs2VD  45288  undif3VD  45329  sineq0ALT  45384  rext0  45386  permac8prim  45462  ndisj2  45503  ralfal  45612  uz0  45861  icccncfext  46336  itgioocnicc  46426  fourierdlem42  46598  fourierdlem62  46617  fourierdlem93  46648  fourierdlem101  46656  nsssmfmbf  47228  aiotavb  47553  afv2ndeffv0  47723  otiunsndisjX  47742  nltle2tri  47776  0nelsetpreimafv  47865  evennodd  48134