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  1674  tbw-bijust  1698  rb-bijust  1749  19.43OLD  1883  cbvexvw  2036  hbn1fw  2045  hba1w  2047  exexw  2051  excom  2162  cbvrexf  3361  cgsex4gOLD  3529  cbvrexcsf  3942  dfss4  4269  neq0f  4348  n0el  4364  ab0ALT  4381  ab0orv  4383  abn0  4385  pssdifcom2  4491  difprsnss  4799  brdif  5196  otthne  5491  otiunsndisj  5525  difopab  5840  difopabOLD  5841  rexiunxp  5851  rexxpf  5858  rnep  5937  somin1  6153  cnvdif  6163  difxp  6184  imadif  6650  brprcneu  6896  brprcneuALT  6897  dffv2  7004  ovima0  7612  porpss  7747  tfinds  7881  poxp  8153  xpord2pred  8170  xpord2indlem  8172  tz7.48lem  8481  brsdom  9015  brsdom2  9137  unfi  9211  fimax2g  9322  ordunifi  9326  dfsup2  9484  supgtoreq  9510  infcllem  9527  suc11reg  9659  rankxplim2  9920  rankxplim3  9921  alephval3  10150  kmlem4  10194  cflim2  10303  isfin4-2  10354  fin23lem25  10364  fin1a2lem5  10444  fin12  10453  axcclem  10497  zorng  10544  infinf  10606  alephadd  10617  fpwwe2  10683  axpre-lttri  11205  dfinfre  12249  infrenegsup  12251  arch  12523  rpneg  13067  xmulcom  13308  xmulneg1  13311  xmulf  13314  xrinfmss2  13353  difreicc  13524  fzp1nel  13651  ssnn0fi  14026  fsuppmapnn0fiubex  14033  hashfun  14476  swrdccatin2  14767  s3iunsndisj  15007  incexc2  15874  lcmftp  16673  f1omvdco3  19467  psgnunilem4  19515  gsumcom3  19996  gsumxp2  19998  0ringnnzr  20525  mdetunilem7  22624  fctop  23011  cctop  23013  ntreq0  23085  ordtbas2  23199  cmpcld  23410  hausdiag  23653  fbun  23848  fbfinnfr  23849  opnfbas  23850  fbasrn  23892  filuni  23893  ufinffr  23937  alexsubALTlem2  24056  ellogdm  26681  nosepon  27710  noextenddif  27713  nomaxmo  27743  nosupinfsep  27777  nocvxminlem  27822  numedglnl  29161  usgredg2v  29244  clwwlknon1nloop  30118  avril1  30482  shne0i  31467  chnlei  31504  cvnbtwn2  32306  cvnbtwn3  32307  cvnbtwn4  32308  chrelat2i  32384  atabs2i  32421  dmdbr5ati  32441  nmo  32509  disjdifprg  32588  eliccelico  32779  elicoelioo  32780  xrdifh  32782  f1ocnt  32804  tosglblem  32964  xrnarchi  33191  elrgspnlem2  33247  fldextrspunlsplem  33723  hasheuni  34086  cntnevol  34229  sitgaddlemb  34350  eulerpartlemgs2  34382  ballotlem2  34491  ballotlemodife  34500  plymulx0  34562  bnj1143  34804  bnj1304  34833  bnj1476  34861  bnj1533  34866  bnj1174  35017  bnj1204  35026  bnj1280  35034  nummin  35105  0nn0m1nnn0  35118  lfuhgr3  35125  erdszelem9  35204  fmla0disjsuc  35403  dftr6  35751  fundmpss  35767  dfon2lem5  35788  dfon2lem8  35791  dfon2lem9  35792  wzel  35825  elfuns  35916  dfrecs2  35951  df3nandALT1  36400  andnand1  36402  imnand2  36403  bj-notalbii  36615  difunieq  37375  domalom  37405  fvineqsneq  37413  fdc  37752  nninfnub  37758  tsbi4  38143  ts3an2  38158  ts3an3  38159  ts3or1  38160  vvdifopab  38261  brvvdif  38264  n0elqs  38327  dfssr2  38500  lcvnbtwn2  39028  lcvnbtwn3  39029  cvrnbtwn3  39277  dalem18  39683  lhpocnel2  40021  cdleme0nex  40292  cdlemk19w  40974  dihglblem6  41342  dvh2dim  41447  dvh3dim3N  41451  aks4d1p7  42084  aks6d1c5  42140  sticksstones1  42147  aks6d1c6lem3  42173  metakunt1  42206  redvmptabs  42390  sn-tz6.12-2  42690  ctbnfien  42829  rencldnfilem  42831  numinfctb  43115  onmaxnelsup  43235  onsupnmax  43240  onsupuni  43241  onsupeqnmax  43259  oenassex  43331  naddgeoa  43407  ifpnorcor  43493  ifpnancor  43494  ifpdfnan  43499  ifpananb  43519  ifpnannanb  43520  ifpxorxorb  43524  rp-isfinite6  43531  pwinfig  43574  elnonrel  43598  iunrelexp0  43715  frege131  44007  frege133  44009  compab  44461  zfregs2VD  44861  undif3VD  44902  sineq0ALT  44957  rext0  44959  ndisj2  45056  ralfal  45166  uz0  45423  icccncfext  45902  itgioocnicc  45992  fourierdlem42  46164  fourierdlem62  46183  fourierdlem93  46214  fourierdlem101  46222  nsssmfmbf  46794  aiotavb  47102  afv2ndeffv0  47272  otiunsndisjX  47291  nltle2tri  47325  0nelsetpreimafv  47377  evennodd  47630