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  1675  tbw-bijust  1699  rb-bijust  1750  19.43OLD  1884  cbvexvw  2038  hbn1fw  2048  hba1w  2050  exexw  2054  excom  2167  cbvrexf  3329  cgsex4gOLD  3486  cbvrexcsf  3890  dfss4  4219  neq0f  4298  n0el  4314  ab0ALT  4331  abn0  4335  pssdifcom2  4441  difprsnss  4753  brdif  5149  otthne  5432  otiunsndisj  5466  difopab  5777  rexiunxp  5787  rexxpf  5794  dm0rn0  5871  rnep  5874  somin1  6088  cnvdif  6099  difxp  6120  imadif  6574  brprcneu  6822  brprcneuALT  6823  dffv2  6927  ovima0  7535  porpss  7670  tfinds  7800  poxp  8068  xpord2pred  8085  xpord2indlem  8087  tz7.48lem  8370  brsdom  8909  brsdom2  9027  unfi  9093  fimax2g  9184  ordunifi  9188  dfsup2  9345  supgtoreq  9372  infcllem  9389  suc11reg  9526  rankxplim2  9790  rankxplim3  9791  alephval3  10018  kmlem4  10062  cflim2  10171  isfin4-2  10222  fin23lem25  10232  fin1a2lem5  10312  fin12  10321  axcclem  10365  zorng  10412  alephadd  10486  fpwwe2  10552  axpre-lttri  11074  dfinfre  12121  infrenegsup  12123  arch  12396  rpneg  12937  xmulcom  13179  xmulneg1  13182  xmulf  13185  xrinfmss2  13224  difreicc  13398  fzp1nel  13525  ssnn0fi  13906  fsuppmapnn0fiubex  13913  hashfun  14358  swrdccatin2  14650  s3iunsndisj  14889  incexc2  15759  lcmftp  16561  f1omvdco3  19376  psgnunilem4  19424  gsumcom3  19905  gsumxp2  19907  0ringnnzr  20456  mdetunilem7  22560  fctop  22946  cctop  22948  ntreq0  23019  ordtbas2  23133  cmpcld  23344  hausdiag  23587  fbun  23782  fbfinnfr  23783  opnfbas  23784  fbasrn  23826  filuni  23827  ufinffr  23871  alexsubALTlem2  23990  ellogdm  26602  nosepon  27631  noextenddif  27634  nomaxmo  27664  nosupinfsep  27698  nocvxminlem  27744  numedglnl  29166  usgredg2v  29249  clwwlknon1nloop  30123  avril1  30487  shne0i  31472  chnlei  31509  cvnbtwn2  32311  cvnbtwn3  32312  cvnbtwn4  32313  chrelat2i  32389  atabs2i  32426  dmdbr5ati  32446  nmo  32513  disjdifprg  32599  eliccelico  32806  elicoelioo  32807  xrdifh  32809  f1ocnt  32829  tosglblem  33005  xrnarchi  33215  elrgspnlem2  33274  fldextrspunlsplem  33779  hasheuni  34191  cntnevol  34334  sitgaddlemb  34454  eulerpartlemgs2  34486  ballotlem2  34595  ballotlemodife  34604  plymulx0  34653  bnj1143  34895  bnj1304  34924  bnj1476  34952  bnj1533  34957  bnj1174  35108  bnj1204  35117  bnj1280  35125  nummin  35198  axreg  35232  axregscl  35233  noinfepregs  35238  axregs  35244  vonf1owev  35251  0nn0m1nnn0  35256  lfuhgr3  35263  erdszelem9  35342  fmla0disjsuc  35541  dftr6  35894  fundmpss  35910  dfon2lem5  35928  dfon2lem8  35931  dfon2lem9  35932  wzel  35965  elfuns  36056  dfrecs2  36093  df3nandALT1  36542  andnand1  36544  imnand2  36545  bj-notalbii  36757  difunieq  37518  domalom  37548  fvineqsneq  37556  fdc  37885  nninfnub  37891  tsbi4  38276  ts3an2  38291  ts3an3  38292  ts3or1  38293  vvdifopab  38397  brvvdif  38400  n0elqs  38464  dfssr2  38691  lcvnbtwn2  39226  lcvnbtwn3  39227  cvrnbtwn3  39475  dalem18  39880  lhpocnel2  40218  cdleme0nex  40489  cdlemk19w  41171  dihglblem6  41539  dvh2dim  41644  dvh3dim3N  41648  aks4d1p7  42276  aks6d1c5  42332  sticksstones1  42339  aks6d1c6lem3  42365  redvmptabs  42557  ctbnfien  43002  rencldnfilem  43004  numinfctb  43287  onmaxnelsup  43407  onsupnmax  43412  onsupuni  43413  onsupeqnmax  43431  oenassex  43502  naddgeoa  43578  ifpnorcor  43663  ifpnancor  43664  ifpdfnan  43669  ifpananb  43689  ifpnannanb  43690  ifpxorxorb  43694  rp-isfinite6  43701  pwinfig  43744  elnonrel  43768  iunrelexp0  43885  frege131  44177  frege133  44179  compab  44624  zfregs2VD  45023  undif3VD  45064  sineq0ALT  45119  rext0  45121  permac8prim  45197  ndisj2  45238  ralfal  45347  uz0  45598  icccncfext  46073  itgioocnicc  46163  fourierdlem42  46335  fourierdlem62  46354  fourierdlem93  46385  fourierdlem101  46393  nsssmfmbf  46965  aiotavb  47278  afv2ndeffv0  47448  otiunsndisjX  47467  nltle2tri  47501  0nelsetpreimafv  47578  evennodd  47831