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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnbi  333  xchnxbi  335  xchbinx  337  oplem1  1072  nic-axALT  1707  tbw-bijust  1731  rb-bijust  1782  19.43OLD  1916  cbvexvw  2070  hbn1fw  2080  hba1w  2082  exexw  2086  excom  2199  cbvrexf  3346  cbvrexcsf  3890  dfss4  4215  neq0f  4295  n0el  4312  ab0ALT  4330  abn0  4334  pssdifcom2  4446  difprsnss  4762  brdif  5158  otthne  5462  otiunsndisj  5497  difopab  5811  rexiunxp  5820  rexxpf  5827  dm0rn0  5908  rnep  5911  somin1  6127  cnvdif  6134  difxp  6156  xpdifcnvepel  6161  imadif  6618  brprcneu  6869  brprcneuALT  6870  dffv2  6974  ovima0  7594  porpss  7729  tfinds  7857  poxp  8127  xpord2pred  8144  xpord2indlem  8146  tz7.48lem  8431  brsdom  8981  brsdom2  9100  unfi  9166  fimax2g  9257  ordunifi  9261  dfsup2  9415  supgtoreq  9442  infcllem  9459  suc11reg  9599  rankxplim2  9863  rankxplim3  9864  alephval3  10114  kmlem4  10157  cflim2  10266  isfin4-2  10317  fin23lem25  10327  fin1a2lem5  10407  fin12  10416  axcclem  10460  zorng  10507  alephadd  10587  fpwwe2  10653  axpre-lttri  11175  dfinfre  12221  infrenegsup  12223  arch  12526  0nn0m1nnn0  12676  rpneg  13077  xmulcom  13319  xmulneg1  13322  xmulf  13325  xrinfmss2  13364  difreicc  13538  fzp1nel  13667  ssnn0fi  14050  fsuppmapnn0fiubex  14057  hashfun  14503  swrdccatin2  14799  s3iunsndisj  15042  incexc2  15928  lcmftp  16727  f1omvdco3  19577  psgnunilem4  19625  gsumcom3  20106  gsumxp2  20108  0ringnnzr  20687  mdetunilem7  22841  fctop  23230  cctop  23232  ntreq0  23303  ordtbas2  23417  cmpcld  23628  hausdiag  23872  fbun  24067  fbfinnfr  24068  opnfbas  24069  fbasrn  24111  filuni  24112  ufinffr  24156  alexsubALTlem2  24275  plyn0mulidp  26512  ellogdm  26877  nosepon  27902  noextenddif  27905  nomaxmo  27935  nosupinfsep  27969  nocvxminlem  28020  bdayfinbndlem1  28733  numedglnl  29602  lfuhgr3  29608  usgredg2v  29688  clwwlknon1nloop  30570  avril1  30944  shne0i  31930  chnlei  31967  cvnbtwn2  32769  cvnbtwn3  32770  cvnbtwn4  32771  chrelat2i  32847  atabs2i  32884  dmdbr5ati  32904  nmo  32966  disjdifprg  33049  eliccelico  33249  elicoelioo  33250  xrdifh  33252  f1ocnt  33272  tosglblem  33415  xrnarchi  33625  elrgspnlem2  33684  fldextrspunlsplem  34184  hasheuni  34596  cntnevol  34740  sitgaddlemb  34860  eulerpartlemgs2  34892  ballotlem2  35001  ballotlemodife  35010  bnj1143  35300  bnj1304  35329  bnj1476  35357  bnj1533  35362  bnj1174  35513  bnj1204  35522  bnj1280  35530  nummin  35599  axreg  35654  axregscl  35655  noinfepregs  35660  axregs  35666  kardexen  35690  vonf1wev  35706  vonf1owevOLD  35708  erdszelem9  35779  fmla0disjsuc  35978  dftr6  36331  fundmpss  36347  dfon2lem5  36365  dfon2lem8  36368  dfon2lem9  36369  wzel  36402  elfuns  36493  dfrecs2  36530  dffr7  36536  df3nandALT1  37019  andnand1  37021  imnand2  37022  regsfromregtco  37158  regsfromunir1  37160  bj-notalbii  37331  difunieq  38129  domalom  38159  fvineqsneq  38167  fdc  38496  nninfnub  38502  tsbi4  38885  ts3an2  38900  ts3an3  38901  ts3or1  38902  vvdifopab  39014  brvvdif  39017  n0elqs  39081  dfssr2  39328  lcvnbtwn2  39901  lcvnbtwn3  39902  cvrnbtwn3  40150  dalem18  40555  lhpocnel2  40893  cdleme0nex  41164  cdlemk19w  41846  dihglblem6  42214  dvh2dim  42319  dvh3dim3N  42323  aks4d1p7  42950  aks6d1c5  43006  sticksstones1  43013  aks6d1c6lem3  43039  redvmptabs  43236  ctbnfien  43660  rencldnfilem  43662  numinfctb  43945  onmaxnelsup  44065  onsupnmax  44070  onsupuni  44071  onsupeqnmax  44089  oenassex  44160  naddgeoa  44236  ifpnorcor  44321  ifpnancor  44322  ifpdfnan  44327  ifpananb  44347  ifpnannanb  44348  ifpxorxorb  44352  rp-isfinite6  44359  pwinfig  44402  elnonrel  44426  iunrelexp0  44543  frege131  44835  frege133  44837  compab  45266  zfregs2VD  45664  undif3VD  45705  sineq0ALT  45760  rext0  45762  permac8prim  45838  ndisj2  45886  ralfal  45994  uz0  46241  icccncfext  46716  itgioocnicc  46806  fourierdlem42  46978  fourierdlem62  46997  fourierdlem93  47028  fourierdlem101  47036  nsssmfmbf  47608  aiotavb  47979  afv2ndeffv0  48149  otiunsndisjX  48168  nltle2tri  48202  0nelsetpreimafv  48291  evennodd  48560