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  3324  cgsex4gOLD  3484  cbvrexcsf  3894  dfss4  4220  neq0f  4299  n0el  4315  ab0ALT  4332  ab0orv  4334  abn0  4336  pssdifcom2  4442  difprsnss  4750  brdif  5145  otthne  5429  otiunsndisj  5463  difopab  5773  rexiunxp  5783  rexxpf  5790  rnep  5869  somin1  6082  cnvdif  6092  difxp  6113  imadif  6566  brprcneu  6812  brprcneuALT  6813  dffv2  6918  ovima0  7528  porpss  7663  tfinds  7793  poxp  8061  xpord2pred  8078  xpord2indlem  8080  tz7.48lem  8363  brsdom  8900  brsdom2  9018  unfi  9085  fimax2g  9175  ordunifi  9179  dfsup2  9334  supgtoreq  9361  infcllem  9378  suc11reg  9515  rankxplim2  9776  rankxplim3  9777  alephval3  10004  kmlem4  10048  cflim2  10157  isfin4-2  10208  fin23lem25  10218  fin1a2lem5  10298  fin12  10307  axcclem  10351  zorng  10398  infinf  10460  alephadd  10471  fpwwe2  10537  axpre-lttri  11059  dfinfre  12106  infrenegsup  12108  arch  12381  rpneg  12927  xmulcom  13168  xmulneg1  13171  xmulf  13174  xrinfmss2  13213  difreicc  13387  fzp1nel  13514  ssnn0fi  13892  fsuppmapnn0fiubex  13899  hashfun  14344  swrdccatin2  14635  s3iunsndisj  14875  incexc2  15745  lcmftp  16547  f1omvdco3  19328  psgnunilem4  19376  gsumcom3  19857  gsumxp2  19859  0ringnnzr  20410  mdetunilem7  22503  fctop  22889  cctop  22891  ntreq0  22962  ordtbas2  23076  cmpcld  23287  hausdiag  23530  fbun  23725  fbfinnfr  23726  opnfbas  23727  fbasrn  23769  filuni  23770  ufinffr  23814  alexsubALTlem2  23933  ellogdm  26546  nosepon  27575  noextenddif  27578  nomaxmo  27608  nosupinfsep  27642  nocvxminlem  27688  numedglnl  29089  usgredg2v  29172  clwwlknon1nloop  30043  avril1  30407  shne0i  31392  chnlei  31429  cvnbtwn2  32231  cvnbtwn3  32232  cvnbtwn4  32233  chrelat2i  32309  atabs2i  32346  dmdbr5ati  32366  nmo  32434  disjdifprg  32519  eliccelico  32720  elicoelioo  32721  xrdifh  32723  f1ocnt  32745  tosglblem  32916  xrnarchi  33126  elrgspnlem2  33183  fldextrspunlsplem  33640  hasheuni  34052  cntnevol  34195  sitgaddlemb  34316  eulerpartlemgs2  34348  ballotlem2  34457  ballotlemodife  34466  plymulx0  34515  bnj1143  34757  bnj1304  34786  bnj1476  34814  bnj1533  34819  bnj1174  34970  bnj1204  34979  bnj1280  34987  nummin  35058  axreg  35062  axregscl  35063  axregs  35078  vonf1owev  35085  0nn0m1nnn0  35090  lfuhgr3  35097  erdszelem9  35176  fmla0disjsuc  35375  dftr6  35728  fundmpss  35744  dfon2lem5  35765  dfon2lem8  35768  dfon2lem9  35769  wzel  35802  elfuns  35893  dfrecs2  35928  df3nandALT1  36377  andnand1  36379  imnand2  36380  bj-notalbii  36592  difunieq  37352  domalom  37382  fvineqsneq  37390  fdc  37729  nninfnub  37735  tsbi4  38120  ts3an2  38135  ts3an3  38136  ts3or1  38137  vvdifopab  38239  brvvdif  38242  n0elqs  38304  dfssr2  38480  lcvnbtwn2  39010  lcvnbtwn3  39011  cvrnbtwn3  39259  dalem18  39664  lhpocnel2  40002  cdleme0nex  40273  cdlemk19w  40955  dihglblem6  41323  dvh2dim  41428  dvh3dim3N  41432  aks4d1p7  42060  aks6d1c5  42116  sticksstones1  42123  aks6d1c6lem3  42149  redvmptabs  42337  sn-tz6.12-2  42657  ctbnfien  42795  rencldnfilem  42797  numinfctb  43080  onmaxnelsup  43200  onsupnmax  43205  onsupuni  43206  onsupeqnmax  43224  oenassex  43295  naddgeoa  43371  ifpnorcor  43457  ifpnancor  43458  ifpdfnan  43463  ifpananb  43483  ifpnannanb  43484  ifpxorxorb  43488  rp-isfinite6  43495  pwinfig  43538  elnonrel  43562  iunrelexp0  43679  frege131  43971  frege133  43973  compab  44419  zfregs2VD  44818  undif3VD  44859  sineq0ALT  44914  rext0  44916  permac8prim  44992  ndisj2  45033  ralfal  45143  uz0  45395  icccncfext  45872  itgioocnicc  45962  fourierdlem42  46134  fourierdlem62  46153  fourierdlem93  46184  fourierdlem101  46192  nsssmfmbf  46764  aiotavb  47078  afv2ndeffv0  47248  otiunsndisjX  47267  nltle2tri  47301  0nelsetpreimafv  47378  evennodd  47631