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  1055  nic-axALT  1669  tbw-bijust  1693  rb-bijust  1744  19.43OLD  1879  cbvexvw  2033  hbn1fw  2041  hba1w  2043  exexw  2047  excom  2152  cbvrexf  3354  cgsex4gOLD  3519  cbvrexcsf  3938  dfss4  4259  indifdirOLD  4286  neq0f  4342  n0el  4362  ab0ALT  4377  ab0orv  4379  abn0  4381  pssdifcom2  4491  difprsnss  4803  brdif  5201  otthne  5488  otiunsndisj  5522  difopab  5832  difopabOLD  5833  rexiunxp  5843  rexxpf  5850  rnep  5929  somin1  6139  cnvdif  6148  difxp  6168  imadif  6637  brprcneu  6887  brprcneuALT  6888  dffv2  6993  ovima0  7600  porpss  7732  tfinds  7864  poxp  8133  xpord2pred  8150  xpord2indlem  8152  tz7.48lem  8462  brsdom  8996  brsdom2  9122  unfi  9197  fimax2g  9314  ordunifi  9318  dfsup2  9468  supgtoreq  9494  infcllem  9511  suc11reg  9643  rankxplim2  9904  rankxplim3  9905  alephval3  10134  kmlem4  10177  cflim2  10287  isfin4-2  10338  fin23lem25  10348  fin1a2lem5  10428  fin12  10437  axcclem  10481  zorng  10528  infinf  10590  alephadd  10601  fpwwe2  10667  axpre-lttri  11189  dfinfre  12226  infrenegsup  12228  arch  12500  rpneg  13039  xmulcom  13278  xmulneg1  13281  xmulf  13284  xrinfmss2  13323  difreicc  13494  fzp1nel  13618  ssnn0fi  13983  fsuppmapnn0fiubex  13990  hashfun  14429  swrdccatin2  14712  s3iunsndisj  14948  incexc2  15817  lcmftp  16607  f1omvdco3  19404  psgnunilem4  19452  gsumcom3  19933  gsumxp2  19935  0ringnnzr  20462  mdetunilem7  22533  fctop  22920  cctop  22922  ntreq0  22994  ordtbas2  23108  cmpcld  23319  hausdiag  23562  fbun  23757  fbfinnfr  23758  opnfbas  23759  fbasrn  23801  filuni  23802  ufinffr  23846  alexsubALTlem2  23965  ellogdm  26586  nosepon  27611  noextenddif  27614  nomaxmo  27644  nosupinfsep  27678  nocvxminlem  27723  numedglnl  28970  usgredg2v  29053  clwwlknon1nloop  29922  avril1  30286  shne0i  31271  chnlei  31308  cvnbtwn2  32110  cvnbtwn3  32111  cvnbtwn4  32112  chrelat2i  32188  atabs2i  32225  dmdbr5ati  32245  nmo  32301  disjdifprg  32378  eliccelico  32558  elicoelioo  32559  xrdifh  32561  f1ocnt  32583  tosglblem  32714  xrnarchi  32905  hasheuni  33704  cntnevol  33847  sitgaddlemb  33968  eulerpartlemgs2  34000  ballotlem2  34108  ballotlemodife  34117  plymulx0  34179  bnj1143  34421  bnj1304  34450  bnj1476  34478  bnj1533  34483  bnj1174  34634  bnj1204  34643  bnj1280  34651  nummin  34714  0nn0m1nnn0  34722  lfuhgr3  34729  erdszelem9  34809  fmla0disjsuc  35008  dftr6  35345  fundmpss  35362  dfon2lem5  35383  dfon2lem8  35386  dfon2lem9  35387  wzel  35420  elfuns  35511  dfrecs2  35546  df3nandALT1  35883  andnand1  35885  imnand2  35886  bj-notalbii  36091  difunieq  36853  domalom  36883  fvineqsneq  36891  fdc  37218  nninfnub  37224  tsbi4  37609  ts3an2  37624  ts3an3  37625  ts3or1  37626  vvdifopab  37732  brvvdif  37735  n0elqs  37798  dfssr2  37971  lcvnbtwn2  38499  lcvnbtwn3  38500  cvrnbtwn3  38748  dalem18  39154  lhpocnel2  39492  cdleme0nex  39763  cdlemk19w  40445  dihglblem6  40813  dvh2dim  40918  dvh3dim3N  40922  aks4d1p7  41554  aks6d1c5  41610  sticksstones1  41618  aks6d1c6lem3  41644  metakunt1  41657  ctbnfien  42238  rencldnfilem  42240  numinfctb  42527  onmaxnelsup  42651  onsupnmax  42656  onsupuni  42657  onsupeqnmax  42675  oenassex  42747  naddgeoa  42824  ifpnorcor  42910  ifpnancor  42911  ifpdfnan  42916  ifpananb  42936  ifpnannanb  42937  ifpxorxorb  42941  rp-isfinite6  42948  pwinfig  42991  elnonrel  43015  iunrelexp0  43132  frege131  43424  frege133  43426  compab  43879  zfregs2VD  44280  undif3VD  44321  sineq0ALT  44376  ndisj2  44415  ralfal  44532  uz0  44794  icccncfext  45275  itgioocnicc  45365  fourierdlem42  45537  fourierdlem62  45556  fourierdlem93  45587  fourierdlem101  45595  nsssmfmbf  46167  aiotavb  46470  afv2ndeffv0  46640  otiunsndisjX  46659  nltle2tri  46693  0nelsetpreimafv  46730  evennodd  46983