Theorem notbii 323

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  sylnbi  333  xchnxbi  335  xchbinx  337  oplem1  1070  nic-axALT  1701  tbw-bijust  1725  rb-bijust  1776  19.43OLD  1910  cbvexvw  2064  hbn1fw  2074  hba1w  2076  exexw  2080  excom  2203  cbvrexf  3357  cbvrexcsf  3904  dfss4  4230  neq0f  4310  n0el  4327  ab0ALT  4344  abn0  4348  pssdifcom2  4456  difprsnss  4771  brdif  5168  otthne  5469  otiunsndisj  5504  difopab  5818  rexiunxp  5827  rexxpf  5834  dm0rn0  5915  rnep  5918  somin1  6134  cnvdif  6141  difxp  6162  xpdifcnvepel  6167  imadif  6621  brprcneu  6872  brprcneuALT  6873  dffv2  6977  ovima0  7590  porpss  7725  tfinds  7856  poxp  8124  xpord2pred  8141  xpord2indlem  8143  tz7.48lem  8428  brsdom  8971  brsdom2  9089  unfi  9155  fimax2g  9246  ordunifi  9250  dfsup2  9404  supgtoreq  9431  infcllem  9448  suc11reg  9588  rankxplim2  9852  rankxplim3  9853  alephval3  10094  kmlem4  10137  cflim2  10247  isfin4-2  10298  fin23lem25  10308  fin1a2lem5  10388  fin12  10397  axcclem  10441  zorng  10488  alephadd  10562  fpwwe2  10628  axpre-lttri  11150  dfinfre  12196  infrenegsup  12198  arch  12501  rpneg  13050  xmulcom  13292  xmulneg1  13295  xmulf  13298  xrinfmss2  13337  difreicc  13511  fzp1nel  13639  ssnn0fi  14021  fsuppmapnn0fiubex  14028  hashfun  14474  swrdccatin2  14766  s3iunsndisj  15005  incexc2  15892  lcmftp  16694  f1omvdco3  19519  psgnunilem4  19567  gsumcom3  20048  gsumxp2  20050  0ringnnzr  20609  mdetunilem7  22744  fctop  23130  cctop  23132  ntreq0  23203  ordtbas2  23317  cmpcld  23528  hausdiag  23771  fbun  23966  fbfinnfr  23967  opnfbas  23968  fbasrn  24010  filuni  24011  ufinffr  24055  alexsubALTlem2  24174  plyn0mulidp  26411  ellogdm  26770  nosepon  27795  noextenddif  27798  nomaxmo  27828  nosupinfsep  27862  nocvxminlem  27913  bdayfinbndlem1  28626  numedglnl  29435  usgredg2v  29518  clwwlknon1nloop  30391  avril1  30755  shne0i  31741  chnlei  31778  cvnbtwn2  32580  cvnbtwn3  32581  cvnbtwn4  32582  chrelat2i  32658  atabs2i  32695  dmdbr5ati  32715  nmo  32777  disjdifprg  32861  eliccelico  33063  elicoelioo  33064  xrdifh  33066  f1ocnt  33086  tosglblem  33235  xrnarchi  33445  elrgspnlem2  33504  fldextrspunlsplem  34008  hasheuni  34420  cntnevol  34563  sitgaddlemb  34683  eulerpartlemgs2  34715  ballotlem2  34824  ballotlemodife  34833  bnj1143  35123  bnj1304  35152  bnj1476  35180  bnj1533  35185  bnj1174  35336  bnj1204  35345  bnj1280  35353  nummin  35427  axreg  35463  axregscl  35464  noinfepregs  35469  axregs  35475  vonf1wev  35491  vonf1owevOLD  35493  0nn0m1nnn0  35503  lfuhgr3  35511  erdszelem9  35590  fmla0disjsuc  35789  dftr6  36142  fundmpss  36158  dfon2lem5  36176  dfon2lem8  36179  dfon2lem9  36180  wzel  36213  elfuns  36304  dfrecs2  36341  df3nandALT1  36799  andnand1  36801  imnand2  36802  regsfromregtco  36938  regsfromunir1  36940  bj-notalbii  37111  difunieq  37908  domalom  37938  fvineqsneq  37946  fdc  38284  nninfnub  38290  tsbi4  38675  ts3an2  38690  ts3an3  38691  ts3or1  38692  vvdifopab  38804  brvvdif  38807  n0elqs  38871  dfssr2  39118  lcvnbtwn2  39691  lcvnbtwn3  39692  cvrnbtwn3  39940  dalem18  40345  lhpocnel2  40683  cdleme0nex  40954  cdlemk19w  41636  dihglblem6  42004  dvh2dim  42109  dvh3dim3N  42113  aks4d1p7  42740  aks6d1c5  42796  sticksstones1  42803  aks6d1c6lem3  42829  redvmptabs  43011  ctbnfien  43437  rencldnfilem  43439  numinfctb  43722  onmaxnelsup  43842  onsupnmax  43847  onsupuni  43848  onsupeqnmax  43866  oenassex  43937  naddgeoa  44013  ifpnorcor  44098  ifpnancor  44099  ifpdfnan  44104  ifpananb  44124  ifpnannanb  44125  ifpxorxorb  44129  rp-isfinite6  44136  pwinfig  44179  elnonrel  44203  iunrelexp0  44320  frege131  44612  frege133  44614  compab  45043  zfregs2VD  45441  undif3VD  45482  sineq0ALT  45537  rext0  45539  permac8prim  45615  ndisj2  45663  ralfal  45771  uz0  46018  icccncfext  46493  itgioocnicc  46583  fourierdlem42  46755  fourierdlem62  46774  fourierdlem93  46805  fourierdlem101  46813  nsssmfmbf  47385  aiotavb  47716  afv2ndeffv0  47886  otiunsndisjX  47905  nltle2tri  47939  0nelsetpreimafv  48028  evennodd  48297