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  3332  cgsex4gOLD  3492  cbvrexcsf  3902  dfss4  4228  neq0f  4307  n0el  4323  ab0ALT  4340  ab0orv  4342  abn0  4344  pssdifcom2  4450  difprsnss  4759  brdif  5155  otthne  5441  otiunsndisj  5475  difopab  5784  rexiunxp  5794  rexxpf  5801  rnep  5880  somin1  6094  cnvdif  6104  difxp  6125  imadif  6584  brprcneu  6830  brprcneuALT  6831  dffv2  6938  ovima0  7548  porpss  7683  tfinds  7816  poxp  8084  xpord2pred  8101  xpord2indlem  8103  tz7.48lem  8386  brsdom  8923  brsdom2  9042  unfi  9112  fimax2g  9209  ordunifi  9213  dfsup2  9371  supgtoreq  9398  infcllem  9415  suc11reg  9548  rankxplim2  9809  rankxplim3  9810  alephval3  10039  kmlem4  10083  cflim2  10192  isfin4-2  10243  fin23lem25  10253  fin1a2lem5  10333  fin12  10342  axcclem  10386  zorng  10433  infinf  10495  alephadd  10506  fpwwe2  10572  axpre-lttri  11094  dfinfre  12140  infrenegsup  12142  arch  12415  rpneg  12961  xmulcom  13202  xmulneg1  13205  xmulf  13208  xrinfmss2  13247  difreicc  13421  fzp1nel  13548  ssnn0fi  13926  fsuppmapnn0fiubex  13933  hashfun  14378  swrdccatin2  14670  s3iunsndisj  14910  incexc2  15780  lcmftp  16582  f1omvdco3  19363  psgnunilem4  19411  gsumcom3  19892  gsumxp2  19894  0ringnnzr  20445  mdetunilem7  22538  fctop  22924  cctop  22926  ntreq0  22997  ordtbas2  23111  cmpcld  23322  hausdiag  23565  fbun  23760  fbfinnfr  23761  opnfbas  23762  fbasrn  23804  filuni  23805  ufinffr  23849  alexsubALTlem2  23968  ellogdm  26581  nosepon  27610  noextenddif  27613  nomaxmo  27643  nosupinfsep  27677  nocvxminlem  27723  numedglnl  29124  usgredg2v  29207  clwwlknon1nloop  30078  avril1  30442  shne0i  31427  chnlei  31464  cvnbtwn2  32266  cvnbtwn3  32267  cvnbtwn4  32268  chrelat2i  32344  atabs2i  32381  dmdbr5ati  32401  nmo  32469  disjdifprg  32554  eliccelico  32750  elicoelioo  32751  xrdifh  32753  f1ocnt  32775  tosglblem  32946  xrnarchi  33153  elrgspnlem2  33210  fldextrspunlsplem  33661  hasheuni  34068  cntnevol  34211  sitgaddlemb  34332  eulerpartlemgs2  34364  ballotlem2  34473  ballotlemodife  34482  plymulx0  34531  bnj1143  34773  bnj1304  34802  bnj1476  34830  bnj1533  34835  bnj1174  34986  bnj1204  34995  bnj1280  35003  nummin  35074  vonf1owev  35088  0nn0m1nnn0  35093  lfuhgr3  35100  erdszelem9  35179  fmla0disjsuc  35378  dftr6  35731  fundmpss  35747  dfon2lem5  35768  dfon2lem8  35771  dfon2lem9  35772  wzel  35805  elfuns  35896  dfrecs2  35931  df3nandALT1  36380  andnand1  36382  imnand2  36383  bj-notalbii  36595  difunieq  37355  domalom  37385  fvineqsneq  37393  fdc  37732  nninfnub  37738  tsbi4  38123  ts3an2  38138  ts3an3  38139  ts3or1  38140  vvdifopab  38242  brvvdif  38245  n0elqs  38307  dfssr2  38483  lcvnbtwn2  39013  lcvnbtwn3  39014  cvrnbtwn3  39262  dalem18  39668  lhpocnel2  40006  cdleme0nex  40277  cdlemk19w  40959  dihglblem6  41327  dvh2dim  41432  dvh3dim3N  41436  aks4d1p7  42064  aks6d1c5  42120  sticksstones1  42127  aks6d1c6lem3  42153  redvmptabs  42341  sn-tz6.12-2  42661  ctbnfien  42799  rencldnfilem  42801  numinfctb  43085  onmaxnelsup  43205  onsupnmax  43210  onsupuni  43211  onsupeqnmax  43229  oenassex  43300  naddgeoa  43376  ifpnorcor  43462  ifpnancor  43463  ifpdfnan  43468  ifpananb  43488  ifpnannanb  43489  ifpxorxorb  43493  rp-isfinite6  43500  pwinfig  43543  elnonrel  43567  iunrelexp0  43684  frege131  43976  frege133  43978  compab  44424  zfregs2VD  44823  undif3VD  44864  sineq0ALT  44919  rext0  44921  permac8prim  44997  ndisj2  45038  ralfal  45148  uz0  45401  icccncfext  45878  itgioocnicc  45968  fourierdlem42  46140  fourierdlem62  46159  fourierdlem93  46190  fourierdlem101  46198  nsssmfmbf  46770  aiotavb  47084  afv2ndeffv0  47254  otiunsndisjX  47273  nltle2tri  47307  0nelsetpreimafv  47384  evennodd  47637