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  1057  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  19.43OLD  1885  cbvexvw  2039  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2168  cbvrexf  3323  cbvrexcsf  3880  dfss4  4209  neq0f  4288  n0el  4304  ab0ALT  4321  abn0  4325  pssdifcom2  4430  difprsnss  4744  brdif  5138  otthne  5439  otiunsndisj  5474  difopab  5786  rexiunxp  5795  rexxpf  5802  dm0rn0  5879  rnep  5882  somin1  6096  cnvdif  6107  difxp  6128  imadif  6582  brprcneu  6830  brprcneuALT  6831  dffv2  6935  ovima0  7546  porpss  7681  tfinds  7811  poxp  8078  xpord2pred  8095  xpord2indlem  8097  tz7.48lem  8380  brsdom  8921  brsdom2  9039  unfi  9105  fimax2g  9196  ordunifi  9200  dfsup2  9357  supgtoreq  9384  infcllem  9401  suc11reg  9540  rankxplim2  9804  rankxplim3  9805  alephval3  10032  kmlem4  10076  cflim2  10185  isfin4-2  10236  fin23lem25  10246  fin1a2lem5  10326  fin12  10335  axcclem  10379  zorng  10426  alephadd  10500  fpwwe2  10566  axpre-lttri  11088  dfinfre  12137  infrenegsup  12139  arch  12434  rpneg  12976  xmulcom  13218  xmulneg1  13221  xmulf  13224  xrinfmss2  13263  difreicc  13437  fzp1nel  13565  ssnn0fi  13947  fsuppmapnn0fiubex  13954  hashfun  14399  swrdccatin2  14691  s3iunsndisj  14930  incexc2  15803  lcmftp  16605  f1omvdco3  19424  psgnunilem4  19472  gsumcom3  19953  gsumxp2  19955  0ringnnzr  20502  mdetunilem7  22583  fctop  22969  cctop  22971  ntreq0  23042  ordtbas2  23156  cmpcld  23367  hausdiag  23610  fbun  23805  fbfinnfr  23806  opnfbas  23807  fbasrn  23849  filuni  23850  ufinffr  23894  alexsubALTlem2  24013  ellogdm  26603  nosepon  27629  noextenddif  27632  nomaxmo  27662  nosupinfsep  27696  nocvxminlem  27746  bdayfinbndlem1  28459  numedglnl  29213  usgredg2v  29296  clwwlknon1nloop  30169  avril1  30533  shne0i  31519  chnlei  31556  cvnbtwn2  32358  cvnbtwn3  32359  cvnbtwn4  32360  chrelat2i  32436  atabs2i  32473  dmdbr5ati  32493  nmo  32559  disjdifprg  32645  eliccelico  32850  elicoelioo  32851  xrdifh  32853  f1ocnt  32873  tosglblem  33034  xrnarchi  33245  elrgspnlem2  33304  fldextrspunlsplem  33817  hasheuni  34229  cntnevol  34372  sitgaddlemb  34492  eulerpartlemgs2  34524  ballotlem2  34633  ballotlemodife  34642  plymulx0  34691  bnj1143  34932  bnj1304  34961  bnj1476  34989  bnj1533  34994  bnj1174  35145  bnj1204  35154  bnj1280  35162  nummin  35236  axreg  35271  axregscl  35272  noinfepregs  35277  axregs  35283  vonf1owev  35290  0nn0m1nnn0  35295  lfuhgr3  35302  erdszelem9  35381  fmla0disjsuc  35580  dftr6  35933  fundmpss  35949  dfon2lem5  35967  dfon2lem8  35970  dfon2lem9  35971  wzel  36004  elfuns  36095  dfrecs2  36132  df3nandALT1  36581  andnand1  36583  imnand2  36584  regsfromregtco  36720  regsfromunir1  36722  bj-notalbii  36894  difunieq  37690  domalom  37720  fvineqsneq  37728  fdc  38066  nninfnub  38072  tsbi4  38457  ts3an2  38472  ts3an3  38473  ts3or1  38474  vvdifopab  38586  brvvdif  38589  n0elqs  38653  dfssr2  38900  lcvnbtwn2  39473  lcvnbtwn3  39474  cvrnbtwn3  39722  dalem18  40127  lhpocnel2  40465  cdleme0nex  40736  cdlemk19w  41418  dihglblem6  41786  dvh2dim  41891  dvh3dim3N  41895  aks4d1p7  42522  aks6d1c5  42578  sticksstones1  42585  aks6d1c6lem3  42611  redvmptabs  42792  ctbnfien  43246  rencldnfilem  43248  numinfctb  43531  onmaxnelsup  43651  onsupnmax  43656  onsupuni  43657  onsupeqnmax  43675  oenassex  43746  naddgeoa  43822  ifpnorcor  43907  ifpnancor  43908  ifpdfnan  43913  ifpananb  43933  ifpnannanb  43934  ifpxorxorb  43938  rp-isfinite6  43945  pwinfig  43988  elnonrel  44012  iunrelexp0  44129  frege131  44421  frege133  44423  compab  44868  zfregs2VD  45267  undif3VD  45308  sineq0ALT  45363  rext0  45365  permac8prim  45441  ndisj2  45482  ralfal  45591  uz0  45840  icccncfext  46315  itgioocnicc  46405  fourierdlem42  46577  fourierdlem62  46596  fourierdlem93  46627  fourierdlem101  46635  nsssmfmbf  47207  aiotavb  47538  afv2ndeffv0  47708  otiunsndisjX  47727  nltle2tri  47761  0nelsetpreimafv  47850  evennodd  48119