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  1918  cbvexvw  2072  hbn1fw  2082  hba1w  2084  exexw  2088  excom  2202  cbvrexf  3350  cbvrexcsf  3894  dfss4  4217  neq0f  4298  n0el  4315  ab0ALT  4333  abn0  4337  pssdifcom2  4449  difprsnss  4764  brdif  5164  otthne  5462  otiunsndisj  5500  difopab  5818  rexiunxp  5827  rexxpf  5835  dm0rn0  5918  rnep  5921  somin1  6145  cnvdif  6152  difxp  6173  xpdifcnvepel  6178  imadif  6654  brprcneu  6906  brprcneuALT  6907  dffv2  7011  ovima0  7632  porpss  7775  tfinds  7905  poxp  8177  xpord2pred  8199  xpord2indlem  8201  tz7.48lemOLD  8489  brsdom  9039  brsdom2  9158  unfi  9224  fimax2g  9315  ordunifi  9319  dfsup2  9473  supgtoreq  9500  infcllem  9517  suc11reg  9657  rankxplim2  9934  rankxplim3  9935  alephval3  10228  kmlem4  10271  cflim2  10380  isfin4-2  10431  fin23lem25  10441  fin1a2lem5  10521  fin12  10530  axcclem  10574  zorng  10621  alephadd  10701  fpwwe2  10767  axpre-lttri  11289  dfinfre  12338  infrenegsup  12340  arch  12643  0nn0m1nnn0  12793  rpneg  13194  xmulcom  13436  xmulneg1  13439  xmulf  13442  xrinfmss2  13481  difreicc  13655  fzp1nel  13785  ssnn0fi  14168  fsuppmapnn0fiubex  14175  hashfun  14623  swrdccatin2  14920  s3iunsndisj  15164  incexc2  16051  lcmftp  16855  f1omvdco3  19714  psgnunilem4  19762  gsumcom3  20243  gsumxp2  20245  0ringnnzr  20827  mdetunilem7  22988  fctop  23377  cctop  23379  ntreq0  23450  ordtbas2  23564  cmpcld  23775  hausdiag  24019  fbun  24214  fbfinnfr  24215  opnfbas  24216  fbasrn  24258  filuni  24259  ufinffr  24303  alexsubALTlem2  24422  plyn0mulidp  26657  ellogdm  27024  nosepon  28079  noextenddif  28082  nomaxmo  28112  nosupinfsep  28146  nocvxminlem  28197  bdayfinbndlem1  28910  numedglnl  29779  lfuhgr3  29785  usgredg2v  29865  clwwlknon1nloop  30747  avril1  31121  shne0i  32107  chnlei  32144  cvnbtwn2  32946  cvnbtwn3  32947  cvnbtwn4  32948  chrelat2i  33024  atabs2i  33061  dmdbr5ati  33081  nmo  33185  disjdifprg  33267  eliccelico  33465  elicoelioo  33466  xrdifh  33468  f1ocnt  33488  tosglblem  33631  xrnarchi  33844  elrgspnlem2  33903  fldextrspunlsplem  34416  hasheuni  34828  cntnevol  34972  sitgaddlemb  35091  eulerpartlemgs2  35123  ballotlem2  35232  ballotlemodife  35241  bnj1143  35531  bnj1304  35560  bnj1476  35588  bnj1533  35593  bnj1174  35744  bnj1204  35753  bnj1280  35761  rmo6  35821  nummin  35847  axreg  35936  axregscl  35937  noinfepregs  35942  axregs  35948  kardexen  35972  vonf1wev  36077  vonf1owevOLD  36079  erdszelem9  36172  fmla0disjsuc  36371  mirimanoffr  36668  mirimanofffr  36670  elpssmo  36673  dftr6  36731  fundmpss  36747  dfon2lem5  36764  dfon2lem8  36767  dfon2lem9  36768  wzel  36801  elfuns  36892  dfrecs2  36929  dffr7  36935  df3nandALT1  37402  andnand1  37404  imnand2  37405  regsfromregtco  37541  regsfromunir1  37543  bj-notalbii  37714  difunieq  38565  domalom  38595  fvineqsneq  38603  fdc  38945  nninfnub  38951  tsbi4  39334  ts3an2  39349  ts3an3  39350  ts3or1  39351  vvdifopab  39463  brvvdif  39466  n0elqs  39530  dfssr2  39777  lcvnbtwn2  40350  lcvnbtwn3  40351  cvrnbtwn3  40599  dalem18  41004  lhpocnel2  41342  cdleme0nex  41613  cdlemk19w  42295  dihglblem6  42663  dvh2dim  42768  dvh3dim3N  42772  aks4d1p7  43399  aks6d1c5  43455  sticksstones1  43462  aks6d1c6lem3  43488  redvmptabs  43677  ctbnfien  44091  rencldnfilem  44093  numinfctb  44370  onmaxnelsup  44486  onsupnmax  44491  onsupuni  44492  onsupeqnmax  44510  oenassex  44581  naddgeoa  44657  ifpnorcor  44742  ifpnancor  44743  ifpdfnan  44748  ifpananb  44768  ifpnannanb  44769  ifpxorxorb  44773  rp-isfinite6  44780  pwinfig  44823  elnonrel  44847  iunrelexp0  44963  frege131  45255  frege133  45257  compab  45685  zfregs2VD  46083  undif3VD  46124  sineq0ALT  46179  rext0  46181  permac8prim  46268  ndisj2  46342  ralfal  46449  uz0  46695  icccncfext  47170  itgioocnicc  47260  fourierdlem42  47432  fourierdlem62  47451  fourierdlem93  47482  fourierdlem101  47490  nsssmfmbf  48062  aiotavb  48433  afv2ndeffv0  48603  otiunsndisjX  48622  nltle2tri  48656  0nelsetpreimafv  48745  evennodd  49014