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  1056  nic-axALT  1674  tbw-bijust  1698  rb-bijust  1749  19.43OLD  1883  cbvexvw  2037  hbn1fw  2046  hba1w  2048  exexw  2052  excom  2163  cbvrexf  3335  cgsex4gOLD  3495  cbvrexcsf  3905  dfss4  4232  neq0f  4311  n0el  4327  ab0ALT  4344  ab0orv  4346  abn0  4348  pssdifcom2  4454  difprsnss  4763  brdif  5160  otthne  5446  otiunsndisj  5480  difopab  5793  difopabOLD  5794  rexiunxp  5804  rexxpf  5811  rnep  5890  somin1  6106  cnvdif  6116  difxp  6137  imadif  6600  brprcneu  6848  brprcneuALT  6849  dffv2  6956  ovima0  7568  porpss  7703  tfinds  7836  poxp  8107  xpord2pred  8124  xpord2indlem  8126  tz7.48lem  8409  brsdom  8946  brsdom2  9065  unfi  9135  fimax2g  9233  ordunifi  9237  dfsup2  9395  supgtoreq  9422  infcllem  9439  suc11reg  9572  rankxplim2  9833  rankxplim3  9834  alephval3  10063  kmlem4  10107  cflim2  10216  isfin4-2  10267  fin23lem25  10277  fin1a2lem5  10357  fin12  10366  axcclem  10410  zorng  10457  infinf  10519  alephadd  10530  fpwwe2  10596  axpre-lttri  11118  dfinfre  12164  infrenegsup  12166  arch  12439  rpneg  12985  xmulcom  13226  xmulneg1  13229  xmulf  13232  xrinfmss2  13271  difreicc  13445  fzp1nel  13572  ssnn0fi  13950  fsuppmapnn0fiubex  13957  hashfun  14402  swrdccatin2  14694  s3iunsndisj  14934  incexc2  15804  lcmftp  16606  f1omvdco3  19379  psgnunilem4  19427  gsumcom3  19908  gsumxp2  19910  0ringnnzr  20434  mdetunilem7  22505  fctop  22891  cctop  22893  ntreq0  22964  ordtbas2  23078  cmpcld  23289  hausdiag  23532  fbun  23727  fbfinnfr  23728  opnfbas  23729  fbasrn  23771  filuni  23772  ufinffr  23816  alexsubALTlem2  23935  ellogdm  26548  nosepon  27577  noextenddif  27580  nomaxmo  27610  nosupinfsep  27644  nocvxminlem  27689  numedglnl  29071  usgredg2v  29154  clwwlknon1nloop  30028  avril1  30392  shne0i  31377  chnlei  31414  cvnbtwn2  32216  cvnbtwn3  32217  cvnbtwn4  32218  chrelat2i  32294  atabs2i  32331  dmdbr5ati  32351  nmo  32419  disjdifprg  32504  eliccelico  32700  elicoelioo  32701  xrdifh  32703  f1ocnt  32725  tosglblem  32900  xrnarchi  33138  elrgspnlem2  33194  fldextrspunlsplem  33668  hasheuni  34075  cntnevol  34218  sitgaddlemb  34339  eulerpartlemgs2  34371  ballotlem2  34480  ballotlemodife  34489  plymulx0  34538  bnj1143  34780  bnj1304  34809  bnj1476  34837  bnj1533  34842  bnj1174  34993  bnj1204  35002  bnj1280  35010  nummin  35081  vonf1owev  35095  0nn0m1nnn0  35100  lfuhgr3  35107  erdszelem9  35186  fmla0disjsuc  35385  dftr6  35738  fundmpss  35754  dfon2lem5  35775  dfon2lem8  35778  dfon2lem9  35779  wzel  35812  elfuns  35903  dfrecs2  35938  df3nandALT1  36387  andnand1  36389  imnand2  36390  bj-notalbii  36602  difunieq  37362  domalom  37392  fvineqsneq  37400  fdc  37739  nninfnub  37745  tsbi4  38130  ts3an2  38145  ts3an3  38146  ts3or1  38147  vvdifopab  38249  brvvdif  38252  n0elqs  38314  dfssr2  38490  lcvnbtwn2  39020  lcvnbtwn3  39021  cvrnbtwn3  39269  dalem18  39675  lhpocnel2  40013  cdleme0nex  40284  cdlemk19w  40966  dihglblem6  41334  dvh2dim  41439  dvh3dim3N  41443  aks4d1p7  42071  aks6d1c5  42127  sticksstones1  42134  aks6d1c6lem3  42160  redvmptabs  42348  sn-tz6.12-2  42668  ctbnfien  42806  rencldnfilem  42808  numinfctb  43092  onmaxnelsup  43212  onsupnmax  43217  onsupuni  43218  onsupeqnmax  43236  oenassex  43307  naddgeoa  43383  ifpnorcor  43469  ifpnancor  43470  ifpdfnan  43475  ifpananb  43495  ifpnannanb  43496  ifpxorxorb  43500  rp-isfinite6  43507  pwinfig  43550  elnonrel  43574  iunrelexp0  43691  frege131  43983  frege133  43985  compab  44431  zfregs2VD  44830  undif3VD  44871  sineq0ALT  44926  rext0  44928  permac8prim  45004  ndisj2  45045  ralfal  45155  uz0  45408  icccncfext  45885  itgioocnicc  45975  fourierdlem42  46147  fourierdlem62  46166  fourierdlem93  46197  fourierdlem101  46205  nsssmfmbf  46777  aiotavb  47091  afv2ndeffv0  47261  otiunsndisjX  47280  nltle2tri  47314  0nelsetpreimafv  47391  evennodd  47644