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  1056  nic-axALT  1675  tbw-bijust  1699  rb-bijust  1750  19.43OLD  1884  cbvexvw  2038  hbn1fw  2048  hba1w  2050  exexw  2054  excom  2165  cbvrexf  3327  cgsex4gOLD  3484  cbvrexcsf  3888  dfss4  4216  neq0f  4295  n0el  4311  ab0ALT  4328  abn0  4332  pssdifcom2  4438  difprsnss  4748  brdif  5142  otthne  5424  otiunsndisj  5458  difopab  5769  rexiunxp  5779  rexxpf  5786  dm0rn0  5863  rnep  5866  somin1  6079  cnvdif  6090  difxp  6111  imadif  6565  brprcneu  6812  brprcneuALT  6813  dffv2  6917  ovima0  7525  porpss  7660  tfinds  7790  poxp  8058  xpord2pred  8075  xpord2indlem  8077  tz7.48lem  8360  brsdom  8897  brsdom2  9014  unfi  9080  fimax2g  9170  ordunifi  9174  dfsup2  9328  supgtoreq  9355  infcllem  9372  suc11reg  9509  rankxplim2  9773  rankxplim3  9774  alephval3  10001  kmlem4  10045  cflim2  10154  isfin4-2  10205  fin23lem25  10215  fin1a2lem5  10295  fin12  10304  axcclem  10348  zorng  10395  infinf  10457  alephadd  10468  fpwwe2  10534  axpre-lttri  11056  dfinfre  12103  infrenegsup  12105  arch  12378  rpneg  12924  xmulcom  13165  xmulneg1  13168  xmulf  13171  xrinfmss2  13210  difreicc  13384  fzp1nel  13511  ssnn0fi  13892  fsuppmapnn0fiubex  13899  hashfun  14344  swrdccatin2  14636  s3iunsndisj  14875  incexc2  15745  lcmftp  16547  f1omvdco3  19361  psgnunilem4  19409  gsumcom3  19890  gsumxp2  19892  0ringnnzr  20440  mdetunilem7  22533  fctop  22919  cctop  22921  ntreq0  22992  ordtbas2  23106  cmpcld  23317  hausdiag  23560  fbun  23755  fbfinnfr  23756  opnfbas  23757  fbasrn  23799  filuni  23800  ufinffr  23844  alexsubALTlem2  23963  ellogdm  26575  nosepon  27604  noextenddif  27607  nomaxmo  27637  nosupinfsep  27671  nocvxminlem  27717  numedglnl  29122  usgredg2v  29205  clwwlknon1nloop  30079  avril1  30443  shne0i  31428  chnlei  31465  cvnbtwn2  32267  cvnbtwn3  32268  cvnbtwn4  32269  chrelat2i  32345  atabs2i  32382  dmdbr5ati  32402  nmo  32469  disjdifprg  32555  eliccelico  32760  elicoelioo  32761  xrdifh  32763  f1ocnt  32782  tosglblem  32955  xrnarchi  33153  elrgspnlem2  33210  fldextrspunlsplem  33686  hasheuni  34098  cntnevol  34241  sitgaddlemb  34361  eulerpartlemgs2  34393  ballotlem2  34502  ballotlemodife  34511  plymulx0  34560  bnj1143  34802  bnj1304  34831  bnj1476  34859  bnj1533  34864  bnj1174  35015  bnj1204  35024  bnj1280  35032  nummin  35104  axreg  35125  axregscl  35126  axregs  35145  vonf1owev  35152  0nn0m1nnn0  35157  lfuhgr3  35164  erdszelem9  35243  fmla0disjsuc  35442  dftr6  35795  fundmpss  35811  dfon2lem5  35829  dfon2lem8  35832  dfon2lem9  35833  wzel  35866  elfuns  35957  dfrecs2  35994  df3nandALT1  36443  andnand1  36445  imnand2  36446  bj-notalbii  36658  difunieq  37418  domalom  37448  fvineqsneq  37456  fdc  37795  nninfnub  37801  tsbi4  38186  ts3an2  38201  ts3an3  38202  ts3or1  38203  vvdifopab  38307  brvvdif  38310  n0elqs  38374  dfssr2  38601  lcvnbtwn2  39136  lcvnbtwn3  39137  cvrnbtwn3  39385  dalem18  39790  lhpocnel2  40128  cdleme0nex  40399  cdlemk19w  41081  dihglblem6  41449  dvh2dim  41554  dvh3dim3N  41558  aks4d1p7  42186  aks6d1c5  42242  sticksstones1  42249  aks6d1c6lem3  42275  redvmptabs  42463  sn-tz6.12-2  42783  ctbnfien  42921  rencldnfilem  42923  numinfctb  43206  onmaxnelsup  43326  onsupnmax  43331  onsupuni  43332  onsupeqnmax  43350  oenassex  43421  naddgeoa  43497  ifpnorcor  43583  ifpnancor  43584  ifpdfnan  43589  ifpananb  43609  ifpnannanb  43610  ifpxorxorb  43614  rp-isfinite6  43621  pwinfig  43664  elnonrel  43688  iunrelexp0  43805  frege131  44097  frege133  44099  compab  44544  zfregs2VD  44943  undif3VD  44984  sineq0ALT  45039  rext0  45041  permac8prim  45117  ndisj2  45158  ralfal  45268  uz0  45520  icccncfext  45995  itgioocnicc  46085  fourierdlem42  46257  fourierdlem62  46276  fourierdlem93  46307  fourierdlem101  46315  nsssmfmbf  46887  aiotavb  47200  afv2ndeffv0  47370  otiunsndisjX  47389  nltle2tri  47423  0nelsetpreimafv  47500  evennodd  47753