Theorem notbii 322

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 321	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	mpbi 232	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  sylnbi  332  xchnxbi  334  xchbinx  336  oplem1  1051  xorcomOLD  1505  xorbi12iOLD  1516  norcomOLD  1523  noranOLD  1527  nororOLD  1529  norassOLD  1534  nic-axALT  1675  tbw-bijust  1699  rb-bijust  1750  19.43OLD  1884  cbvexvw  2044  hbn1fw  2052  hba1w  2054  excom  2169  sbnvOLD  2322  cbvexv1  2362  cbvex2v  2365  cbvrexfw  3438  cbvrexf  3440  cbvrexcsf  3926  dfss4  4235  indifdir  4260  neq0f  4306  n0el  4321  ab0  4333  pssdifcom2  4436  difprsnss  4732  brdif  5119  otiunsndisj  5410  difopab  5702  rexiunxp  5711  rexxpf  5718  rnep  5797  somin1  5993  cnvdif  6002  difxp  6021  imadif  6438  brprcneu  6662  dffv2  6756  ovima0  7327  porpss  7453  tfinds  7574  poxp  7822  tz7.48lem  8077  brsdom  8532  brsdom2  8641  fimax2g  8764  ordunifi  8768  dfsup2  8908  supgtoreq  8934  infcllem  8951  suc11reg  9082  rankxplim2  9309  rankxplim3  9310  alephval3  9536  kmlem4  9579  cflim2  9685  isfin4-2  9736  fin23lem25  9746  fin1a2lem5  9826  fin12  9835  axcclem  9879  zorng  9926  infinf  9988  alephadd  9999  fpwwe2  10065  axpre-lttri  10587  dfinfre  11622  infrenegsup  11624  arch  11895  rpneg  12422  xmulcom  12660  xmulneg1  12663  xmulf  12666  xrinfmss2  12705  difreicc  12871  fzp1nel  12992  ssnn0fi  13354  fsuppmapnn0fiubex  13361  hashfun  13799  swrdccatin2  14091  s3iunsndisj  14328  incexc2  15193  lcmftp  15980  f1omvdco3  18577  psgnunilem4  18625  gsumcom3  19098  gsumxp2  19100  0ringnnzr  20042  mdetunilem7  21227  fctop  21612  cctop  21614  ntreq0  21685  ordtbas2  21799  cmpcld  22010  hausdiag  22253  fbun  22448  fbfinnfr  22449  opnfbas  22450  fbasrn  22492  filuni  22493  ufinffr  22537  alexsubALTlem2  22656  ellogdm  25222  numedglnl  26929  usgredg2v  27009  clwwlknon1nloop  27878  avril1  28242  shne0i  29225  chnlei  29262  cvnbtwn2  30064  cvnbtwn3  30065  cvnbtwn4  30066  chrelat2i  30142  atabs2i  30179  dmdbr5ati  30199  nelbOLD  30232  nmo  30254  disjdifprg  30325  eliccelico  30500  elicoelioo  30501  xrdifh  30503  f1ocnt  30525  tosglblem  30656  xrnarchi  30813  hasheuni  31344  cntnevol  31487  sitgaddlemb  31606  eulerpartlemgs2  31638  ballotlem2  31746  ballotlemodife  31755  plymulx0  31817  bnj1143  32062  bnj1304  32091  bnj1476  32119  bnj1533  32124  bnj1174  32275  bnj1204  32284  bnj1280  32292  0nn0m1nnn0  32351  lfuhgr3  32366  erdszelem9  32446  fmla0disjsuc  32645  dftr6  32986  fundmpss  33009  dfon2lem5  33032  dfon2lem8  33035  dfon2lem9  33036  wzel  33111  nosepon  33172  noextenddif  33175  nomaxmo  33201  nocvxminlem  33247  elfuns  33376  dfrecs2  33411  df3nandALT1  33747  andnand1  33749  imnand2  33750  bj-notalbii  33948  difunieq  34658  domalom  34688  fvineqsneq  34696  wl-dfrexv  34864  wl-dfrexex  34865  fdc  35035  nninfnub  35041  tsbi4  35429  ts3an2  35444  ts3an3  35445  ts3or1  35446  vvdifopab  35536  brvvdif  35539  n0elqs  35598  dfssr2  35754  lcvnbtwn2  36178  lcvnbtwn3  36179  cvrnbtwn3  36427  dalem18  36832  lhpocnel2  37170  cdleme0nex  37441  cdlemk19w  38123  dihglblem6  38491  dvh2dim  38596  dvh3dim3N  38600  ctbnfien  39464  rencldnfilem  39466  numinfctb  39752  ifpnorcor  39895  ifpnancor  39896  ifpdfnan  39901  ifpananb  39921  ifpnannanb  39922  ifpxorxorb  39926  rp-isfinite6  39933  pwinfig  39969  elnonrel  39994  iunrelexp0  40096  frege131  40389  frege133  40391  compab  40823  zfregs2VD  41224  undif3VD  41265  sineq0ALT  41320  ndisj2  41362  uz0  41735  icccncfext  42219  itgioocnicc  42311  fourierdlem42  42483  fourierdlem62  42502  fourierdlem93  42533  fourierdlem101  42541  nsssmfmbf  43104  aiotavb  43339  afv2ndeffv0  43508  otiunsndisjX  43527  nltle2tri  43562  0nelsetpreimafv  43599  evennodd  43857  setrec2lem1  44845