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 229	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  sylnbi  330  xchnxbi  332  xchbinx  334  oplem1  1056  xorcomOLD  1514  xorbi12iOLD  1525  norcomOLD  1532  nic-axALT  1677  tbw-bijust  1701  rb-bijust  1752  19.43OLD  1887  cbvexvw  2041  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2163  cbvrexf  3358  cgsex4gOLD  3522  cbvrexcsf  3940  dfss4  4259  indifdirOLD  4286  neq0f  4342  n0el  4362  ab0ALT  4377  ab0orv  4379  abn0  4381  pssdifcom2  4491  difprsnss  4803  brdif  5202  otthne  5487  otiunsndisj  5521  difopab  5831  difopabOLD  5832  rexiunxp  5841  rexxpf  5848  rnep  5927  somin1  6135  cnvdif  6144  difxp  6164  imadif  6633  brprcneu  6882  brprcneuALT  6883  dffv2  6987  ovima0  7586  porpss  7717  tfinds  7849  poxp  8114  xpord2pred  8131  xpord2indlem  8133  tz7.48lem  8441  brsdom  8971  brsdom2  9097  unfi  9172  fimax2g  9289  ordunifi  9293  dfsup2  9439  supgtoreq  9465  infcllem  9482  suc11reg  9614  rankxplim2  9875  rankxplim3  9876  alephval3  10105  kmlem4  10148  cflim2  10258  isfin4-2  10309  fin23lem25  10319  fin1a2lem5  10399  fin12  10408  axcclem  10452  zorng  10499  infinf  10561  alephadd  10572  fpwwe2  10638  axpre-lttri  11160  dfinfre  12195  infrenegsup  12197  arch  12469  rpneg  13006  xmulcom  13245  xmulneg1  13248  xmulf  13251  xrinfmss2  13290  difreicc  13461  fzp1nel  13585  ssnn0fi  13950  fsuppmapnn0fiubex  13957  hashfun  14397  swrdccatin2  14679  s3iunsndisj  14915  incexc2  15784  lcmftp  16573  f1omvdco3  19317  psgnunilem4  19365  gsumcom3  19846  gsumxp2  19848  0ringnnzr  20302  mdetunilem7  22120  fctop  22507  cctop  22509  ntreq0  22581  ordtbas2  22695  cmpcld  22906  hausdiag  23149  fbun  23344  fbfinnfr  23345  opnfbas  23346  fbasrn  23388  filuni  23389  ufinffr  23433  alexsubALTlem2  23552  ellogdm  26147  nosepon  27168  noextenddif  27171  nomaxmo  27201  nosupinfsep  27235  nocvxminlem  27279  numedglnl  28404  usgredg2v  28484  clwwlknon1nloop  29352  avril1  29716  shne0i  30701  chnlei  30738  cvnbtwn2  31540  cvnbtwn3  31541  cvnbtwn4  31542  chrelat2i  31618  atabs2i  31655  dmdbr5ati  31675  nmo  31730  disjdifprg  31806  eliccelico  31988  elicoelioo  31989  xrdifh  31991  f1ocnt  32013  tosglblem  32144  xrnarchi  32330  hasheuni  33083  cntnevol  33226  sitgaddlemb  33347  eulerpartlemgs2  33379  ballotlem2  33487  ballotlemodife  33496  plymulx0  33558  bnj1143  33801  bnj1304  33830  bnj1476  33858  bnj1533  33863  bnj1174  34014  bnj1204  34023  bnj1280  34031  nummin  34094  0nn0m1nnn0  34102  lfuhgr3  34110  erdszelem9  34190  fmla0disjsuc  34389  dftr6  34721  fundmpss  34738  dfon2lem5  34759  dfon2lem8  34762  dfon2lem9  34763  wzel  34796  elfuns  34887  dfrecs2  34922  df3nandALT1  35284  andnand1  35286  imnand2  35287  bj-notalbii  35492  difunieq  36255  domalom  36285  fvineqsneq  36293  fdc  36613  nninfnub  36619  tsbi4  37004  ts3an2  37019  ts3an3  37020  ts3or1  37021  vvdifopab  37128  brvvdif  37131  n0elqs  37195  dfssr2  37369  lcvnbtwn2  37897  lcvnbtwn3  37898  cvrnbtwn3  38146  dalem18  38552  lhpocnel2  38890  cdleme0nex  39161  cdlemk19w  39843  dihglblem6  40211  dvh2dim  40316  dvh3dim3N  40320  aks4d1p7  40948  sticksstones1  40962  metakunt1  40985  ctbnfien  41556  rencldnfilem  41558  numinfctb  41845  onmaxnelsup  41972  onsupnmax  41977  onsupuni  41978  onsupeqnmax  41996  oenassex  42068  naddgeoa  42145  ifpnorcor  42231  ifpnancor  42232  ifpdfnan  42237  ifpananb  42257  ifpnannanb  42258  ifpxorxorb  42262  rp-isfinite6  42269  pwinfig  42312  elnonrel  42336  iunrelexp0  42453  frege131  42745  frege133  42747  compab  43201  zfregs2VD  43602  undif3VD  43643  sineq0ALT  43698  ndisj2  43738  ralfal  43855  uz0  44122  icccncfext  44603  itgioocnicc  44693  fourierdlem42  44865  fourierdlem62  44884  fourierdlem93  44915  fourierdlem101  44923  nsssmfmbf  45495  aiotavb  45798  afv2ndeffv0  45968  otiunsndisjX  45987  nltle2tri  46021  0nelsetpreimafv  46058  evennodd  46311