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 229	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  sylnbi  330  xchnxbi  332  xchbinx  334  oplem1  1056  xorcomOLD  1514  xorbi12iOLD  1525  norcomOLD  1532  nic-axALT  1677  tbw-bijust  1701  rb-bijust  1752  19.43OLD  1887  cbvexvw  2041  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2163  cbvrexf  3358  cgsex4gOLD  3522  cbvrexcsf  3940  dfss4  4259  indifdirOLD  4286  neq0f  4342  n0el  4362  ab0ALT  4377  ab0orv  4379  abn0  4381  pssdifcom2  4491  difprsnss  4803  brdif  5202  otthne  5487  otiunsndisj  5521  difopab  5831  difopabOLD  5832  rexiunxp  5841  rexxpf  5848  rnep  5927  somin1  6135  cnvdif  6144  difxp  6164  imadif  6633  brprcneu  6882  brprcneuALT  6883  dffv2  6987  ovima0  7586  porpss  7717  tfinds  7849  poxp  8114  xpord2pred  8131  xpord2indlem  8133  tz7.48lem  8441  brsdom  8971  brsdom2  9097  unfi  9172  fimax2g  9289  ordunifi  9293  dfsup2  9439  supgtoreq  9465  infcllem  9482  suc11reg  9614  rankxplim2  9875  rankxplim3  9876  alephval3  10105  kmlem4  10148  cflim2  10258  isfin4-2  10309  fin23lem25  10319  fin1a2lem5  10399  fin12  10408  axcclem  10452  zorng  10499  infinf  10561  alephadd  10572  fpwwe2  10638  axpre-lttri  11160  dfinfre  12195  infrenegsup  12197  arch  12469  rpneg  13006  xmulcom  13245  xmulneg1  13248  xmulf  13251  xrinfmss2  13290  difreicc  13461  fzp1nel  13585  ssnn0fi  13950  fsuppmapnn0fiubex  13957  hashfun  14397  swrdccatin2  14679  s3iunsndisj  14915  incexc2  15784  lcmftp  16573  f1omvdco3  19317  psgnunilem4  19365  gsumcom3  19846  gsumxp2  19848  0ringnnzr  20302  mdetunilem7  22120  fctop  22507  cctop  22509  ntreq0  22581  ordtbas2  22695  cmpcld  22906  hausdiag  23149  fbun  23344  fbfinnfr  23345  opnfbas  23346  fbasrn  23388  filuni  23389  ufinffr  23433  alexsubALTlem2  23552  ellogdm  26147  nosepon  27168  noextenddif  27171  nomaxmo  27201  nosupinfsep  27235  nocvxminlem  27279  numedglnl  28435  usgredg2v  28515  clwwlknon1nloop  29383  avril1  29747  shne0i  30732  chnlei  30769  cvnbtwn2  31571  cvnbtwn3  31572  cvnbtwn4  31573  chrelat2i  31649  atabs2i  31686  dmdbr5ati  31706  nmo  31761  disjdifprg  31837  eliccelico  32019  elicoelioo  32020  xrdifh  32022  f1ocnt  32044  tosglblem  32175  xrnarchi  32361  hasheuni  33114  cntnevol  33257  sitgaddlemb  33378  eulerpartlemgs2  33410  ballotlem2  33518  ballotlemodife  33527  plymulx0  33589  bnj1143  33832  bnj1304  33861  bnj1476  33889  bnj1533  33894  bnj1174  34045  bnj1204  34054  bnj1280  34062  nummin  34125  0nn0m1nnn0  34133  lfuhgr3  34141  erdszelem9  34221  fmla0disjsuc  34420  dftr6  34752  fundmpss  34769  dfon2lem5  34790  dfon2lem8  34793  dfon2lem9  34794  wzel  34827  elfuns  34918  dfrecs2  34953  df3nandALT1  35332  andnand1  35334  imnand2  35335  bj-notalbii  35540  difunieq  36303  domalom  36333  fvineqsneq  36341  fdc  36661  nninfnub  36667  tsbi4  37052  ts3an2  37067  ts3an3  37068  ts3or1  37069  vvdifopab  37176  brvvdif  37179  n0elqs  37243  dfssr2  37417  lcvnbtwn2  37945  lcvnbtwn3  37946  cvrnbtwn3  38194  dalem18  38600  lhpocnel2  38938  cdleme0nex  39209  cdlemk19w  39891  dihglblem6  40259  dvh2dim  40364  dvh3dim3N  40368  aks4d1p7  40996  sticksstones1  41010  metakunt1  41033  ctbnfien  41604  rencldnfilem  41606  numinfctb  41893  onmaxnelsup  42020  onsupnmax  42025  onsupuni  42026  onsupeqnmax  42044  oenassex  42116  naddgeoa  42193  ifpnorcor  42279  ifpnancor  42280  ifpdfnan  42285  ifpananb  42305  ifpnannanb  42306  ifpxorxorb  42310  rp-isfinite6  42317  pwinfig  42360  elnonrel  42384  iunrelexp0  42501  frege131  42793  frege133  42795  compab  43249  zfregs2VD  43650  undif3VD  43691  sineq0ALT  43746  ndisj2  43786  ralfal  43903  uz0  44170  icccncfext  44651  itgioocnicc  44741  fourierdlem42  44913  fourierdlem62  44932  fourierdlem93  44963  fourierdlem101  44971  nsssmfmbf  45543  aiotavb  45846  afv2ndeffv0  46016  otiunsndisjX  46035  nltle2tri  46069  0nelsetpreimafv  46106  evennodd  46359