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  1054  xorcomOLD  1510  xorbi12iOLD  1521  norcomOLD  1528  norassOLD  1536  nic-axALT  1677  tbw-bijust  1701  rb-bijust  1752  19.43OLD  1887  cbvexvw  2041  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2163  cbvrexf  3373  cgsex4g  3477  cbvrexcsf  3879  dfss4  4193  indifdirOLD  4220  neq0f  4276  n0el  4296  ab0ALT  4311  ab0orv  4313  abn0  4315  pssdifcom2  4422  difprsnss  4733  brdif  5128  otiunsndisj  5435  difopab  5742  difopabOLD  5743  rexiunxp  5752  rexxpf  5759  rnep  5839  somin1  6043  cnvdif  6052  difxp  6072  imadif  6525  brprcneu  6773  brprcneuALT  6774  dffv2  6872  ovima0  7460  porpss  7589  tfinds  7715  poxp  7978  tz7.48lem  8281  brsdom  8772  brsdom2  8893  unfi  8964  fimax2g  9069  ordunifi  9073  dfsup2  9212  supgtoreq  9238  infcllem  9255  suc11reg  9386  rankxplim2  9647  rankxplim3  9648  alephval3  9875  kmlem4  9918  cflim2  10028  isfin4-2  10079  fin23lem25  10089  fin1a2lem5  10169  fin12  10178  axcclem  10222  zorng  10269  infinf  10331  alephadd  10342  fpwwe2  10408  axpre-lttri  10930  dfinfre  11965  infrenegsup  11967  arch  12239  rpneg  12771  xmulcom  13009  xmulneg1  13012  xmulf  13015  xrinfmss2  13054  difreicc  13225  fzp1nel  13349  ssnn0fi  13714  fsuppmapnn0fiubex  13721  hashfun  14161  swrdccatin2  14451  s3iunsndisj  14688  incexc2  15559  lcmftp  16350  f1omvdco3  19066  psgnunilem4  19114  gsumcom3  19588  gsumxp2  19590  0ringnnzr  20549  mdetunilem7  21776  fctop  22163  cctop  22165  ntreq0  22237  ordtbas2  22351  cmpcld  22562  hausdiag  22805  fbun  23000  fbfinnfr  23001  opnfbas  23002  fbasrn  23044  filuni  23045  ufinffr  23089  alexsubALTlem2  23208  ellogdm  25803  numedglnl  27523  usgredg2v  27603  clwwlknon1nloop  28472  avril1  28836  shne0i  29819  chnlei  29856  cvnbtwn2  30658  cvnbtwn3  30659  cvnbtwn4  30660  chrelat2i  30736  atabs2i  30773  dmdbr5ati  30793  nelbOLDOLD  30826  nmo  30847  disjdifprg  30923  eliccelico  31107  elicoelioo  31108  xrdifh  31110  f1ocnt  31132  tosglblem  31261  xrnarchi  31447  hasheuni  32062  cntnevol  32205  sitgaddlemb  32324  eulerpartlemgs2  32356  ballotlem2  32464  ballotlemodife  32473  plymulx0  32535  bnj1143  32779  bnj1304  32808  bnj1476  32836  bnj1533  32841  bnj1174  32992  bnj1204  33001  bnj1280  33009  nummin  33072  0nn0m1nnn0  33080  lfuhgr3  33090  erdszelem9  33170  fmla0disjsuc  33369  dftr6  33727  fundmpss  33749  dfon2lem5  33772  dfon2lem8  33775  dfon2lem9  33776  xpord2pred  33801  xpord2ind  33803  wzel  33827  nosepon  33877  noextenddif  33880  nomaxmo  33910  nosupinfsep  33944  nocvxminlem  33981  elfuns  34226  dfrecs2  34261  df3nandALT1  34597  andnand1  34599  imnand2  34600  bj-notalbii  34805  difunieq  35554  domalom  35584  fvineqsneq  35592  fdc  35912  nninfnub  35918  tsbi4  36303  ts3an2  36318  ts3an3  36319  ts3or1  36320  vvdifopab  36407  brvvdif  36410  n0elqs  36468  dfssr2  36624  lcvnbtwn2  37048  lcvnbtwn3  37049  cvrnbtwn3  37297  dalem18  37702  lhpocnel2  38040  cdleme0nex  38311  cdlemk19w  38993  dihglblem6  39361  dvh2dim  39466  dvh3dim3N  39470  aks4d1p7  40098  sticksstones1  40109  metakunt1  40132  ctbnfien  40647  rencldnfilem  40649  numinfctb  40935  ifpnorcor  41094  ifpnancor  41095  ifpdfnan  41100  ifpananb  41120  ifpnannanb  41121  ifpxorxorb  41125  rp-isfinite6  41132  pwinfig  41175  elnonrel  41200  iunrelexp0  41317  frege131  41609  frege133  41611  compab  42067  zfregs2VD  42468  undif3VD  42509  sineq0ALT  42564  ndisj2  42606  uz0  42959  icccncfext  43435  itgioocnicc  43525  fourierdlem42  43697  fourierdlem62  43716  fourierdlem93  43747  fourierdlem101  43755  nsssmfmbf  44324  aiotavb  44593  afv2ndeffv0  44763  otiunsndisjX  44782  nltle2tri  44816  0nelsetpreimafv  44853  evennodd  45106