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  2200  cbvrexf  3352  cbvrexcsf  3897  dfss4  4222  neq0f  4302  n0el  4319  ab0ALT  4337  abn0  4341  pssdifcom2  4453  difprsnss  4769  brdif  5166  otthne  5470  otiunsndisj  5505  difopab  5819  rexiunxp  5828  rexxpf  5835  dm0rn0  5916  rnep  5919  somin1  6135  cnvdif  6142  difxp  6163  xpdifcnvepel  6168  imadif  6624  brprcneu  6875  brprcneuALT  6876  dffv2  6980  ovima0  7599  porpss  7734  tfinds  7862  poxp  8130  xpord2pred  8147  xpord2indlem  8149  tz7.48lem  8434  brsdom  8977  brsdom2  9096  unfi  9162  fimax2g  9253  ordunifi  9257  dfsup2  9411  supgtoreq  9438  infcllem  9455  suc11reg  9595  rankxplim2  9859  rankxplim3  9860  alephval3  10110  kmlem4  10153  cflim2  10262  isfin4-2  10313  fin23lem25  10323  fin1a2lem5  10403  fin12  10412  axcclem  10456  zorng  10503  alephadd  10579  fpwwe2  10645  axpre-lttri  11167  dfinfre  12213  infrenegsup  12215  arch  12518  0nn0m1nnn0  12668  rpneg  13068  xmulcom  13310  xmulneg1  13313  xmulf  13316  xrinfmss2  13355  difreicc  13529  fzp1nel  13658  ssnn0fi  14041  fsuppmapnn0fiubex  14048  hashfun  14494  swrdccatin2  14790  s3iunsndisj  15031  incexc2  15917  lcmftp  16718  f1omvdco3  19565  psgnunilem4  19613  gsumcom3  20094  gsumxp2  20096  0ringnnzr  20675  mdetunilem7  22827  fctop  23213  cctop  23215  ntreq0  23286  ordtbas2  23400  cmpcld  23611  hausdiag  23855  fbun  24050  fbfinnfr  24051  opnfbas  24052  fbasrn  24094  filuni  24095  ufinffr  24139  alexsubALTlem2  24258  plyn0mulidp  26495  ellogdm  26857  nosepon  27882  noextenddif  27885  nomaxmo  27915  nosupinfsep  27949  nocvxminlem  28000  bdayfinbndlem1  28713  numedglnl  29551  lfuhgr3  29557  usgredg2v  29637  clwwlknon1nloop  30519  avril1  30887  shne0i  31873  chnlei  31910  cvnbtwn2  32712  cvnbtwn3  32713  cvnbtwn4  32714  chrelat2i  32790  atabs2i  32827  dmdbr5ati  32847  nmo  32909  disjdifprg  32993  eliccelico  33194  elicoelioo  33195  xrdifh  33197  f1ocnt  33217  tosglblem  33360  xrnarchi  33570  elrgspnlem2  33629  fldextrspunlsplem  34129  hasheuni  34541  cntnevol  34685  sitgaddlemb  34805  eulerpartlemgs2  34837  ballotlem2  34946  ballotlemodife  34955  bnj1143  35245  bnj1304  35274  bnj1476  35302  bnj1533  35307  bnj1174  35458  bnj1204  35467  bnj1280  35475  nummin  35544  axreg  35599  axregscl  35600  noinfepregs  35605  axregs  35611  kardexen  35635  vonf1wev  35651  vonf1owevOLD  35653  erdszelem9  35730  fmla0disjsuc  35929  dftr6  36282  fundmpss  36298  dfon2lem5  36316  dfon2lem8  36319  dfon2lem9  36320  wzel  36353  elfuns  36444  dfrecs2  36481  df3nandALT1  36969  andnand1  36971  imnand2  36972  regsfromregtco  37108  regsfromunir1  37110  bj-notalbii  37281  difunieq  38079  domalom  38109  fvineqsneq  38117  fdc  38456  nninfnub  38462  tsbi4  38845  ts3an2  38860  ts3an3  38861  ts3or1  38862  vvdifopab  38974  brvvdif  38977  n0elqs  39041  dfssr2  39288  lcvnbtwn2  39861  lcvnbtwn3  39862  cvrnbtwn3  40110  dalem18  40515  lhpocnel2  40853  cdleme0nex  41124  cdlemk19w  41806  dihglblem6  42174  dvh2dim  42279  dvh3dim3N  42283  aks4d1p7  42910  aks6d1c5  42966  sticksstones1  42973  aks6d1c6lem3  42999  redvmptabs  43181  ctbnfien  43605  rencldnfilem  43607  numinfctb  43890  onmaxnelsup  44010  onsupnmax  44015  onsupuni  44016  onsupeqnmax  44034  oenassex  44105  naddgeoa  44181  ifpnorcor  44266  ifpnancor  44267  ifpdfnan  44272  ifpananb  44292  ifpnannanb  44293  ifpxorxorb  44297  rp-isfinite6  44304  pwinfig  44347  elnonrel  44371  iunrelexp0  44488  frege131  44780  frege133  44782  compab  45211  zfregs2VD  45609  undif3VD  45650  sineq0ALT  45705  rext0  45707  permac8prim  45783  ndisj2  45831  ralfal  45939  uz0  46186  icccncfext  46661  itgioocnicc  46751  fourierdlem42  46923  fourierdlem62  46942  fourierdlem93  46973  fourierdlem101  46981  nsssmfmbf  47553  aiotavb  47887  afv2ndeffv0  48057  otiunsndisjX  48076  nltle2tri  48110  0nelsetpreimafv  48199  evennodd  48468