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  1674  tbw-bijust  1698  rb-bijust  1749  19.43OLD  1883  cbvexvw  2037  hbn1fw  2046  hba1w  2048  exexw  2052  excom  2163  cbvrexf  3337  cgsex4gOLD  3498  cbvrexcsf  3908  dfss4  4235  neq0f  4314  n0el  4330  ab0ALT  4347  ab0orv  4349  abn0  4351  pssdifcom2  4457  difprsnss  4766  brdif  5163  otthne  5449  otiunsndisj  5483  difopab  5796  difopabOLD  5797  rexiunxp  5807  rexxpf  5814  rnep  5893  somin1  6109  cnvdif  6119  difxp  6140  imadif  6603  brprcneu  6851  brprcneuALT  6852  dffv2  6959  ovima0  7571  porpss  7706  tfinds  7839  poxp  8110  xpord2pred  8127  xpord2indlem  8129  tz7.48lem  8412  brsdom  8949  brsdom2  9071  unfi  9141  fimax2g  9240  ordunifi  9244  dfsup2  9402  supgtoreq  9429  infcllem  9446  suc11reg  9579  rankxplim2  9840  rankxplim3  9841  alephval3  10070  kmlem4  10114  cflim2  10223  isfin4-2  10274  fin23lem25  10284  fin1a2lem5  10364  fin12  10373  axcclem  10417  zorng  10464  infinf  10526  alephadd  10537  fpwwe2  10603  axpre-lttri  11125  dfinfre  12171  infrenegsup  12173  arch  12446  rpneg  12992  xmulcom  13233  xmulneg1  13236  xmulf  13239  xrinfmss2  13278  difreicc  13452  fzp1nel  13579  ssnn0fi  13957  fsuppmapnn0fiubex  13964  hashfun  14409  swrdccatin2  14701  s3iunsndisj  14941  incexc2  15811  lcmftp  16613  f1omvdco3  19386  psgnunilem4  19434  gsumcom3  19915  gsumxp2  19917  0ringnnzr  20441  mdetunilem7  22512  fctop  22898  cctop  22900  ntreq0  22971  ordtbas2  23085  cmpcld  23296  hausdiag  23539  fbun  23734  fbfinnfr  23735  opnfbas  23736  fbasrn  23778  filuni  23779  ufinffr  23823  alexsubALTlem2  23942  ellogdm  26555  nosepon  27584  noextenddif  27587  nomaxmo  27617  nosupinfsep  27651  nocvxminlem  27696  numedglnl  29078  usgredg2v  29161  clwwlknon1nloop  30035  avril1  30399  shne0i  31384  chnlei  31421  cvnbtwn2  32223  cvnbtwn3  32224  cvnbtwn4  32225  chrelat2i  32301  atabs2i  32338  dmdbr5ati  32358  nmo  32426  disjdifprg  32511  eliccelico  32707  elicoelioo  32708  xrdifh  32710  f1ocnt  32732  tosglblem  32907  xrnarchi  33145  elrgspnlem2  33201  fldextrspunlsplem  33675  hasheuni  34082  cntnevol  34225  sitgaddlemb  34346  eulerpartlemgs2  34378  ballotlem2  34487  ballotlemodife  34496  plymulx0  34545  bnj1143  34787  bnj1304  34816  bnj1476  34844  bnj1533  34849  bnj1174  35000  bnj1204  35009  bnj1280  35017  nummin  35088  vonf1owev  35102  0nn0m1nnn0  35107  lfuhgr3  35114  erdszelem9  35193  fmla0disjsuc  35392  dftr6  35745  fundmpss  35761  dfon2lem5  35782  dfon2lem8  35785  dfon2lem9  35786  wzel  35819  elfuns  35910  dfrecs2  35945  df3nandALT1  36394  andnand1  36396  imnand2  36397  bj-notalbii  36609  difunieq  37369  domalom  37399  fvineqsneq  37407  fdc  37746  nninfnub  37752  tsbi4  38137  ts3an2  38152  ts3an3  38153  ts3or1  38154  vvdifopab  38256  brvvdif  38259  n0elqs  38321  dfssr2  38497  lcvnbtwn2  39027  lcvnbtwn3  39028  cvrnbtwn3  39276  dalem18  39682  lhpocnel2  40020  cdleme0nex  40291  cdlemk19w  40973  dihglblem6  41341  dvh2dim  41446  dvh3dim3N  41450  aks4d1p7  42078  aks6d1c5  42134  sticksstones1  42141  aks6d1c6lem3  42167  redvmptabs  42355  sn-tz6.12-2  42675  ctbnfien  42813  rencldnfilem  42815  numinfctb  43099  onmaxnelsup  43219  onsupnmax  43224  onsupuni  43225  onsupeqnmax  43243  oenassex  43314  naddgeoa  43390  ifpnorcor  43476  ifpnancor  43477  ifpdfnan  43482  ifpananb  43502  ifpnannanb  43503  ifpxorxorb  43507  rp-isfinite6  43514  pwinfig  43557  elnonrel  43581  iunrelexp0  43698  frege131  43990  frege133  43992  compab  44438  zfregs2VD  44837  undif3VD  44878  sineq0ALT  44933  rext0  44935  permac8prim  45011  ndisj2  45052  ralfal  45162  uz0  45415  icccncfext  45892  itgioocnicc  45982  fourierdlem42  46154  fourierdlem62  46173  fourierdlem93  46204  fourierdlem101  46212  nsssmfmbf  46784  aiotavb  47095  afv2ndeffv0  47265  otiunsndisjX  47284  nltle2tri  47318  0nelsetpreimafv  47395  evennodd  47648