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  1674  tbw-bijust  1698  rb-bijust  1749  19.43OLD  1883  cbvexvw  2036  hbn1fw  2045  hba1w  2047  exexw  2051  excom  2162  cbvrexf  3340  cgsex4gOLD  3508  cbvrexcsf  3917  dfss4  4244  neq0f  4323  n0el  4339  ab0ALT  4356  ab0orv  4358  abn0  4360  pssdifcom2  4466  difprsnss  4775  brdif  5172  otthne  5461  otiunsndisj  5495  difopab  5809  difopabOLD  5810  rexiunxp  5820  rexxpf  5827  rnep  5906  somin1  6122  cnvdif  6132  difxp  6153  imadif  6620  brprcneu  6866  brprcneuALT  6867  dffv2  6974  ovima0  7586  porpss  7721  tfinds  7855  poxp  8127  xpord2pred  8144  xpord2indlem  8146  tz7.48lem  8455  brsdom  8989  brsdom2  9111  unfi  9185  fimax2g  9294  ordunifi  9298  dfsup2  9456  supgtoreq  9483  infcllem  9500  suc11reg  9633  rankxplim2  9894  rankxplim3  9895  alephval3  10124  kmlem4  10168  cflim2  10277  isfin4-2  10328  fin23lem25  10338  fin1a2lem5  10418  fin12  10427  axcclem  10471  zorng  10518  infinf  10580  alephadd  10591  fpwwe2  10657  axpre-lttri  11179  dfinfre  12223  infrenegsup  12225  arch  12498  rpneg  13041  xmulcom  13282  xmulneg1  13285  xmulf  13288  xrinfmss2  13327  difreicc  13501  fzp1nel  13628  ssnn0fi  14003  fsuppmapnn0fiubex  14010  hashfun  14455  swrdccatin2  14747  s3iunsndisj  14987  incexc2  15854  lcmftp  16655  f1omvdco3  19430  psgnunilem4  19478  gsumcom3  19959  gsumxp2  19961  0ringnnzr  20485  mdetunilem7  22556  fctop  22942  cctop  22944  ntreq0  23015  ordtbas2  23129  cmpcld  23340  hausdiag  23583  fbun  23778  fbfinnfr  23779  opnfbas  23780  fbasrn  23822  filuni  23823  ufinffr  23867  alexsubALTlem2  23986  ellogdm  26600  nosepon  27629  noextenddif  27632  nomaxmo  27662  nosupinfsep  27696  nocvxminlem  27741  numedglnl  29123  usgredg2v  29206  clwwlknon1nloop  30080  avril1  30444  shne0i  31429  chnlei  31466  cvnbtwn2  32268  cvnbtwn3  32269  cvnbtwn4  32270  chrelat2i  32346  atabs2i  32383  dmdbr5ati  32403  nmo  32471  disjdifprg  32556  eliccelico  32754  elicoelioo  32755  xrdifh  32757  f1ocnt  32779  tosglblem  32954  xrnarchi  33182  elrgspnlem2  33238  fldextrspunlsplem  33714  hasheuni  34116  cntnevol  34259  sitgaddlemb  34380  eulerpartlemgs2  34412  ballotlem2  34521  ballotlemodife  34530  plymulx0  34579  bnj1143  34821  bnj1304  34850  bnj1476  34878  bnj1533  34883  bnj1174  35034  bnj1204  35043  bnj1280  35051  nummin  35122  0nn0m1nnn0  35135  lfuhgr3  35142  erdszelem9  35221  fmla0disjsuc  35420  dftr6  35768  fundmpss  35784  dfon2lem5  35805  dfon2lem8  35808  dfon2lem9  35809  wzel  35842  elfuns  35933  dfrecs2  35968  df3nandALT1  36417  andnand1  36419  imnand2  36420  bj-notalbii  36632  difunieq  37392  domalom  37422  fvineqsneq  37430  fdc  37769  nninfnub  37775  tsbi4  38160  ts3an2  38175  ts3an3  38176  ts3or1  38177  vvdifopab  38278  brvvdif  38281  n0elqs  38344  dfssr2  38517  lcvnbtwn2  39045  lcvnbtwn3  39046  cvrnbtwn3  39294  dalem18  39700  lhpocnel2  40038  cdleme0nex  40309  cdlemk19w  40991  dihglblem6  41359  dvh2dim  41464  dvh3dim3N  41468  aks4d1p7  42096  aks6d1c5  42152  sticksstones1  42159  aks6d1c6lem3  42185  metakunt1  42218  redvmptabs  42403  sn-tz6.12-2  42703  ctbnfien  42841  rencldnfilem  42843  numinfctb  43127  onmaxnelsup  43247  onsupnmax  43252  onsupuni  43253  onsupeqnmax  43271  oenassex  43342  naddgeoa  43418  ifpnorcor  43504  ifpnancor  43505  ifpdfnan  43510  ifpananb  43530  ifpnannanb  43531  ifpxorxorb  43535  rp-isfinite6  43542  pwinfig  43585  elnonrel  43609  iunrelexp0  43726  frege131  44018  frege133  44020  compab  44466  zfregs2VD  44865  undif3VD  44906  sineq0ALT  44961  rext0  44963  ndisj2  45075  ralfal  45185  uz0  45439  icccncfext  45916  itgioocnicc  46006  fourierdlem42  46178  fourierdlem62  46197  fourierdlem93  46228  fourierdlem101  46236  nsssmfmbf  46808  aiotavb  47119  afv2ndeffv0  47289  otiunsndisjX  47308  nltle2tri  47342  0nelsetpreimafv  47404  evennodd  47657