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  3440  cbvrexf  3442  cbvrexcsf  3928  dfss4  4237  indifdir  4262  neq0f  4308  n0el  4323  ab0  4335  pssdifcom2  4438  difprsnss  4734  brdif  5121  otiunsndisj  5412  difopab  5704  rexiunxp  5713  rexxpf  5720  rnep  5799  somin1  5995  cnvdif  6004  difxp  6023  imadif  6440  brprcneu  6664  dffv2  6758  ovima0  7329  porpss  7455  tfinds  7576  poxp  7824  tz7.48lem  8079  brsdom  8534  brsdom2  8643  fimax2g  8766  ordunifi  8770  dfsup2  8910  supgtoreq  8936  infcllem  8953  suc11reg  9084  rankxplim2  9311  rankxplim3  9312  alephval3  9538  kmlem4  9581  cflim2  9687  isfin4-2  9738  fin23lem25  9748  fin1a2lem5  9828  fin12  9837  axcclem  9881  zorng  9928  infinf  9990  alephadd  10001  fpwwe2  10067  axpre-lttri  10589  dfinfre  11624  infrenegsup  11626  arch  11897  rpneg  12424  xmulcom  12662  xmulneg1  12665  xmulf  12668  xrinfmss2  12707  difreicc  12873  fzp1nel  12994  ssnn0fi  13356  fsuppmapnn0fiubex  13363  hashfun  13801  swrdccatin2  14093  s3iunsndisj  14330  incexc2  15195  lcmftp  15982  f1omvdco3  18579  psgnunilem4  18627  gsumcom3  19100  gsumxp2  19102  0ringnnzr  20044  mdetunilem7  21229  fctop  21614  cctop  21616  ntreq0  21687  ordtbas2  21801  cmpcld  22012  hausdiag  22255  fbun  22450  fbfinnfr  22451  opnfbas  22452  fbasrn  22494  filuni  22495  ufinffr  22539  alexsubALTlem2  22658  ellogdm  25224  numedglnl  26931  usgredg2v  27011  clwwlknon1nloop  27880  avril1  28244  shne0i  29227  chnlei  29264  cvnbtwn2  30066  cvnbtwn3  30067  cvnbtwn4  30068  chrelat2i  30144  atabs2i  30181  dmdbr5ati  30201  nelbOLD  30234  nmo  30256  disjdifprg  30327  eliccelico  30502  elicoelioo  30503  xrdifh  30505  f1ocnt  30527  tosglblem  30658  xrnarchi  30815  hasheuni  31346  cntnevol  31489  sitgaddlemb  31608  eulerpartlemgs2  31640  ballotlem2  31748  ballotlemodife  31757  plymulx0  31819  bnj1143  32064  bnj1304  32093  bnj1476  32121  bnj1533  32126  bnj1174  32277  bnj1204  32286  bnj1280  32294  0nn0m1nnn0  32353  lfuhgr3  32368  erdszelem9  32448  fmla0disjsuc  32647  dftr6  32988  fundmpss  33011  dfon2lem5  33034  dfon2lem8  33037  dfon2lem9  33038  wzel  33113  nosepon  33174  noextenddif  33177  nomaxmo  33203  nocvxminlem  33249  elfuns  33378  dfrecs2  33413  df3nandALT1  33749  andnand1  33751  imnand2  33752  bj-notalbii  33950  difunieq  34657  domalom  34687  fvineqsneq  34695  wl-dfrexv  34851  wl-dfrexex  34852  fdc  35022  nninfnub  35028  tsbi4  35416  ts3an2  35431  ts3an3  35432  ts3or1  35433  vvdifopab  35523  brvvdif  35526  n0elqs  35585  dfssr2  35741  lcvnbtwn2  36165  lcvnbtwn3  36166  cvrnbtwn3  36414  dalem18  36819  lhpocnel2  37157  cdleme0nex  37428  cdlemk19w  38110  dihglblem6  38478  dvh2dim  38583  dvh3dim3N  38587  ctbnfien  39422  rencldnfilem  39424  numinfctb  39710  ifpnorcor  39853  ifpnancor  39854  ifpdfnan  39859  ifpananb  39879  ifpnannanb  39880  ifpxorxorb  39884  rp-isfinite6  39891  pwinfig  39927  elnonrel  39952  iunrelexp0  40054  frege131  40347  frege133  40349  compab  40781  zfregs2VD  41182  undif3VD  41223  sineq0ALT  41278  ndisj2  41320  uz0  41693  icccncfext  42177  itgioocnicc  42269  fourierdlem42  42441  fourierdlem62  42460  fourierdlem93  42491  fourierdlem101  42499  nsssmfmbf  43062  aiotavb  43297  afv2ndeffv0  43466  otiunsndisjX  43485  nltle2tri  43520  0nelsetpreimafv  43557  evennodd  43815  setrec2lem1  44803