Theorem notbii 312

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

Syntax hints:  ¬ wn 3   ↔ wb 198

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 199

This theorem is referenced by:  sylnbi  322  xchnxbi  324  xchbinx  326  oplem1  1085  nanassOLD  1638  xorcom  1642  xorbi12i  1652  nic-axALT  1775  tbw-bijust  1799  rb-bijust  1850  19.43OLD  1988  cbvexvw  2146  hbn1fw  2149  hba1w  2151  excom  2214  sbnv  2336  cbvexv1  2370  cbvrexf  3377  cbvrexcsf  3789  symdifassOLD  4079  dfss4  4087  indifdir  4112  neq0f  4155  n0el  4168  ab0  4180  pssdifcom2  4277  difprsnss  4547  brdif  4925  otiunsndisj  5205  difopab  5485  rexiunxp  5494  rexxpf  5501  somin1  5770  cnvdif  5779  difxp  5798  imadif  6205  brprcneu  6424  dffv2  6517  ovima0  7072  porpss  7200  tfinds  7319  poxp  7552  tz7.48lem  7801  brsdom  8244  brsdom2  8352  fimax2g  8474  ordunifi  8478  dfsup2  8618  supgtoreq  8644  infcllem  8661  suc11reg  8792  rankxplim2  9019  rankxplim3  9020  alephval3  9245  kmlem4  9289  cflim2  9399  isfin4-2  9450  fin23lem25  9460  fin1a2lem5  9540  fin12  9549  axcclem  9593  zorng  9640  infinf  9702  alephadd  9713  fpwwe2  9779  axpre-lttri  10301  dfinfre  11333  infrenegsup  11335  arch  11614  rpneg  12145  xmulcom  12383  xmulneg1  12386  xmulf  12389  xrinfmss2  12428  difreicc  12596  fzp1nel  12717  ssnn0fi  13078  fsuppmapnn0fiubex  13085  hashfun  13512  swrdccatin2  13825  s3iunsndisj  14085  incexc2  14943  lcmftp  15721  f1omvdco3  18218  psgnunilem4  18267  0ringnnzr  19629  gsumcom3  20571  mdetunilem7  20791  fctop  21178  cctop  21180  ntreq0  21251  ordtbas2  21365  cmpcld  21575  hausdiag  21818  fbun  22013  fbfinnfr  22014  opnfbas  22015  fbasrn  22057  filuni  22058  ufinffr  22102  alexsubALTlem2  22221  ellogdm  24783  numedglnl  26442  usgredg2v  26522  clwwlknon1nloop  27472  avril1  27876  shne0i  28861  chnlei  28898  cvnbtwn2  29700  cvnbtwn3  29701  cvnbtwn4  29702  chrelat2i  29778  atabs2i  29815  dmdbr5ati  29835  nmo  29879  difrab2  29886  disjdifprg  29934  eliccelico  30085  elicoelioo  30086  xrdifh  30088  f1ocnt  30105  tosglblem  30213  xrnarchi  30282  hasheuni  30691  cntnevol  30835  sitgaddlemb  30954  eulerpartlemgs2  30986  ballotlem2  31095  ballotlemodife  31104  plymulx0  31170  bnj1143  31406  bnj1304  31435  bnj1476  31462  bnj1533  31467  bnj1174  31616  bnj1204  31625  bnj1280  31633  erdszelem9  31726  dftr6  32181  fundmpss  32205  dfon2lem5  32229  dfon2lem8  32232  dfon2lem9  32233  wzel  32307  nosepon  32356  noextenddif  32359  nomaxmo  32385  nocvxminlem  32431  elfuns  32560  dfrecs2  32595  df3nandALT1  32931  andnand1  32933  imnand2  32934  bj-notalbii  33126  bj-cbvex2v  33270  fdc  34082  nninfnub  34088  tsbi4  34482  ts3an2  34497  ts3an3  34498  ts3or1  34499  vvdifopab  34577  brvvdif  34580  n0elqs  34645  dfssr2  34796  lcvnbtwn2  35101  lcvnbtwn3  35102  cvrnbtwn3  35350  dalem18  35755  lhpocnel2  36093  cdleme0nex  36364  cdlemk19w  37046  dihglblem6  37414  dvh2dim  37519  dvh3dim3N  37523  ctbnfien  38225  rencldnfilem  38227  numinfctb  38515  ifpnorcor  38666  ifpnancor  38667  ifpdfnan  38672  ifpananb  38692  ifpnannanb  38693  ifpxorxorb  38697  rp-isfinite6  38704  pwinfig  38706  elnonrel  38731  iunrelexp0  38834  frege131  39127  frege133  39129  compab  39483  zfregs2VD  39894  undif3VD  39935  sineq0ALT  39990  ndisj2  40034  disjrnmpt2  40182  uz0  40433  icccncfext  40894  itgioocnicc  40986  fourierdlem42  41159  fourierdlem62  41178  fourierdlem93  41209  fourierdlem101  41217  nsssmfmbf  41780  aiotavb  41986  afv2ndeffv0  42161  otiunsndisjX  42181  nltle2tri  42210  evennodd  42385  setrec2lem1  43334