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  1670  tbw-bijust  1694  rb-bijust  1745  19.43OLD  1880  cbvexvw  2033  hbn1fw  2042  hba1w  2044  exexw  2048  excom  2159  cbvrexf  3358  cgsex4gOLD  3526  cbvrexcsf  3953  dfss4  4274  neq0f  4353  n0el  4369  ab0ALT  4386  ab0orv  4388  abn0  4390  pssdifcom2  4496  difprsnss  4803  brdif  5200  otthne  5496  otiunsndisj  5529  difopab  5842  difopabOLD  5843  rexiunxp  5853  rexxpf  5860  rnep  5939  somin1  6155  cnvdif  6165  difxp  6185  imadif  6651  brprcneu  6896  brprcneuALT  6897  dffv2  7003  ovima0  7611  porpss  7745  tfinds  7880  poxp  8151  xpord2pred  8168  xpord2indlem  8170  tz7.48lem  8479  brsdom  9013  brsdom2  9135  unfi  9209  fimax2g  9319  ordunifi  9323  dfsup2  9481  supgtoreq  9507  infcllem  9524  suc11reg  9656  rankxplim2  9917  rankxplim3  9918  alephval3  10147  kmlem4  10191  cflim2  10300  isfin4-2  10351  fin23lem25  10361  fin1a2lem5  10441  fin12  10450  axcclem  10494  zorng  10541  infinf  10603  alephadd  10614  fpwwe2  10680  axpre-lttri  11202  dfinfre  12246  infrenegsup  12248  arch  12520  rpneg  13064  xmulcom  13304  xmulneg1  13307  xmulf  13310  xrinfmss2  13349  difreicc  13520  fzp1nel  13647  ssnn0fi  14022  fsuppmapnn0fiubex  14029  hashfun  14472  swrdccatin2  14763  s3iunsndisj  15003  incexc2  15870  lcmftp  16669  f1omvdco3  19481  psgnunilem4  19529  gsumcom3  20010  gsumxp2  20012  0ringnnzr  20541  mdetunilem7  22639  fctop  23026  cctop  23028  ntreq0  23100  ordtbas2  23214  cmpcld  23425  hausdiag  23668  fbun  23863  fbfinnfr  23864  opnfbas  23865  fbasrn  23907  filuni  23908  ufinffr  23952  alexsubALTlem2  24071  ellogdm  26695  nosepon  27724  noextenddif  27727  nomaxmo  27757  nosupinfsep  27791  nocvxminlem  27836  numedglnl  29175  usgredg2v  29258  clwwlknon1nloop  30127  avril1  30491  shne0i  31476  chnlei  31513  cvnbtwn2  32315  cvnbtwn3  32316  cvnbtwn4  32317  chrelat2i  32393  atabs2i  32430  dmdbr5ati  32450  nmo  32517  disjdifprg  32594  eliccelico  32785  elicoelioo  32786  xrdifh  32788  f1ocnt  32809  tosglblem  32948  xrnarchi  33173  elrgspnlem2  33232  hasheuni  34065  cntnevol  34208  sitgaddlemb  34329  eulerpartlemgs2  34361  ballotlem2  34469  ballotlemodife  34478  plymulx0  34540  bnj1143  34782  bnj1304  34811  bnj1476  34839  bnj1533  34844  bnj1174  34995  bnj1204  35004  bnj1280  35012  nummin  35083  0nn0m1nnn0  35096  lfuhgr3  35103  erdszelem9  35183  fmla0disjsuc  35382  dftr6  35730  fundmpss  35747  dfon2lem5  35768  dfon2lem8  35771  dfon2lem9  35772  wzel  35805  elfuns  35896  dfrecs2  35931  df3nandALT1  36381  andnand1  36383  imnand2  36384  bj-notalbii  36596  difunieq  37356  domalom  37386  fvineqsneq  37394  fdc  37731  nninfnub  37737  tsbi4  38122  ts3an2  38137  ts3an3  38138  ts3or1  38139  vvdifopab  38241  brvvdif  38244  n0elqs  38307  dfssr2  38480  lcvnbtwn2  39008  lcvnbtwn3  39009  cvrnbtwn3  39257  dalem18  39663  lhpocnel2  40001  cdleme0nex  40272  cdlemk19w  40954  dihglblem6  41322  dvh2dim  41427  dvh3dim3N  41431  aks4d1p7  42064  aks6d1c5  42120  sticksstones1  42127  aks6d1c6lem3  42153  metakunt1  42186  redvmptabs  42368  sn-tz6.12-2  42666  ctbnfien  42805  rencldnfilem  42807  numinfctb  43091  onmaxnelsup  43211  onsupnmax  43216  onsupuni  43217  onsupeqnmax  43235  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  44437  zfregs2VD  44838  undif3VD  44879  sineq0ALT  44934  ndisj2  44990  ralfal  45103  uz0  45361  icccncfext  45842  itgioocnicc  45932  fourierdlem42  46104  fourierdlem62  46123  fourierdlem93  46154  fourierdlem101  46162  nsssmfmbf  46734  aiotavb  47039  afv2ndeffv0  47209  otiunsndisjX  47228  nltle2tri  47262  0nelsetpreimafv  47314  evennodd  47567