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  1672  tbw-bijust  1696  rb-bijust  1747  19.43OLD  1882  cbvexvw  2036  hbn1fw  2045  hba1w  2047  exexw  2051  excom  2163  cbvrexf  3369  cgsex4gOLD  3539  cbvrexcsf  3967  dfss4  4288  neq0f  4371  n0el  4387  ab0ALT  4404  ab0orv  4406  abn0  4408  pssdifcom2  4514  difprsnss  4824  brdif  5219  otthne  5506  otiunsndisj  5539  difopab  5854  difopabOLD  5855  rexiunxp  5865  rexxpf  5872  rnep  5951  somin1  6165  cnvdif  6175  difxp  6195  imadif  6662  brprcneu  6910  brprcneuALT  6911  dffv2  7017  ovima0  7629  porpss  7762  tfinds  7897  poxp  8169  xpord2pred  8186  xpord2indlem  8188  tz7.48lem  8497  brsdom  9035  brsdom2  9163  unfi  9238  fimax2g  9350  ordunifi  9354  dfsup2  9513  supgtoreq  9539  infcllem  9556  suc11reg  9688  rankxplim2  9949  rankxplim3  9950  alephval3  10179  kmlem4  10223  cflim2  10332  isfin4-2  10383  fin23lem25  10393  fin1a2lem5  10473  fin12  10482  axcclem  10526  zorng  10573  infinf  10635  alephadd  10646  fpwwe2  10712  axpre-lttri  11234  dfinfre  12276  infrenegsup  12278  arch  12550  rpneg  13089  xmulcom  13328  xmulneg1  13331  xmulf  13334  xrinfmss2  13373  difreicc  13544  fzp1nel  13668  ssnn0fi  14036  fsuppmapnn0fiubex  14043  hashfun  14486  swrdccatin2  14777  s3iunsndisj  15017  incexc2  15886  lcmftp  16683  f1omvdco3  19491  psgnunilem4  19539  gsumcom3  20020  gsumxp2  20022  0ringnnzr  20551  mdetunilem7  22645  fctop  23032  cctop  23034  ntreq0  23106  ordtbas2  23220  cmpcld  23431  hausdiag  23674  fbun  23869  fbfinnfr  23870  opnfbas  23871  fbasrn  23913  filuni  23914  ufinffr  23958  alexsubALTlem2  24077  ellogdm  26699  nosepon  27728  noextenddif  27731  nomaxmo  27761  nosupinfsep  27795  nocvxminlem  27840  numedglnl  29179  usgredg2v  29262  clwwlknon1nloop  30131  avril1  30495  shne0i  31480  chnlei  31517  cvnbtwn2  32319  cvnbtwn3  32320  cvnbtwn4  32321  chrelat2i  32397  atabs2i  32434  dmdbr5ati  32454  nmo  32518  disjdifprg  32597  eliccelico  32782  elicoelioo  32783  xrdifh  32785  f1ocnt  32807  tosglblem  32947  xrnarchi  33164  hasheuni  34049  cntnevol  34192  sitgaddlemb  34313  eulerpartlemgs2  34345  ballotlem2  34453  ballotlemodife  34462  plymulx0  34524  bnj1143  34766  bnj1304  34795  bnj1476  34823  bnj1533  34828  bnj1174  34979  bnj1204  34988  bnj1280  34996  nummin  35067  0nn0m1nnn0  35080  lfuhgr3  35087  erdszelem9  35167  fmla0disjsuc  35366  dftr6  35713  fundmpss  35730  dfon2lem5  35751  dfon2lem8  35754  dfon2lem9  35755  wzel  35788  elfuns  35879  dfrecs2  35914  df3nandALT1  36365  andnand1  36367  imnand2  36368  bj-notalbii  36580  difunieq  37340  domalom  37370  fvineqsneq  37378  fdc  37705  nninfnub  37711  tsbi4  38096  ts3an2  38111  ts3an3  38112  ts3or1  38113  vvdifopab  38216  brvvdif  38219  n0elqs  38282  dfssr2  38455  lcvnbtwn2  38983  lcvnbtwn3  38984  cvrnbtwn3  39232  dalem18  39638  lhpocnel2  39976  cdleme0nex  40247  cdlemk19w  40929  dihglblem6  41297  dvh2dim  41402  dvh3dim3N  41406  aks4d1p7  42040  aks6d1c5  42096  sticksstones1  42103  aks6d1c6lem3  42129  metakunt1  42162  sn-tz6.12-2  42635  ctbnfien  42774  rencldnfilem  42776  numinfctb  43060  onmaxnelsup  43184  onsupnmax  43189  onsupuni  43190  onsupeqnmax  43208  oenassex  43280  naddgeoa  43356  ifpnorcor  43442  ifpnancor  43443  ifpdfnan  43448  ifpananb  43468  ifpnannanb  43469  ifpxorxorb  43473  rp-isfinite6  43480  pwinfig  43523  elnonrel  43547  iunrelexp0  43664  frege131  43956  frege133  43958  compab  44411  zfregs2VD  44812  undif3VD  44853  sineq0ALT  44908  ndisj2  44953  ralfal  45066  uz0  45327  icccncfext  45808  itgioocnicc  45898  fourierdlem42  46070  fourierdlem62  46089  fourierdlem93  46120  fourierdlem101  46128  nsssmfmbf  46700  aiotavb  47005  afv2ndeffv0  47175  otiunsndisjX  47194  nltle2tri  47228  0nelsetpreimafv  47264  evennodd  47517