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  3347  cbvrexcsf  3890  dfss4  4215  neq0f  4295  n0el  4312  ab0ALT  4330  abn0  4334  pssdifcom2  4446  difprsnss  4762  brdif  5158  otthne  5455  otiunsndisj  5493  difopab  5808  rexiunxp  5817  rexxpf  5825  dm0rn0  5906  rnep  5909  somin1  6127  cnvdif  6134  difxp  6155  xpdifcnvepel  6160  imadif  6624  brprcneu  6875  brprcneuALT  6876  dffv2  6980  ovima0  7600  porpss  7743  tfinds  7871  poxp  8140  xpord2pred  8162  xpord2indlem  8164  tz7.48lemOLD  8451  brsdom  9001  brsdom2  9120  unfi  9186  fimax2g  9277  ordunifi  9281  dfsup2  9436  supgtoreq  9463  infcllem  9480  suc11reg  9620  rankxplim2  9897  rankxplim3  9898  alephval3  10189  kmlem4  10232  cflim2  10341  isfin4-2  10392  fin23lem25  10402  fin1a2lem5  10482  fin12  10491  axcclem  10535  zorng  10582  alephadd  10662  fpwwe2  10728  axpre-lttri  11250  dfinfre  12298  infrenegsup  12300  arch  12603  0nn0m1nnn0  12753  rpneg  13154  xmulcom  13396  xmulneg1  13399  xmulf  13402  xrinfmss2  13441  difreicc  13615  fzp1nel  13745  ssnn0fi  14128  fsuppmapnn0fiubex  14135  hashfun  14582  swrdccatin2  14878  s3iunsndisj  15121  incexc2  16007  lcmftp  16811  f1omvdco3  19663  psgnunilem4  19711  gsumcom3  20192  gsumxp2  20194  0ringnnzr  20776  mdetunilem7  22933  fctop  23322  cctop  23324  ntreq0  23395  ordtbas2  23509  cmpcld  23720  hausdiag  23964  fbun  24159  fbfinnfr  24160  opnfbas  24161  fbasrn  24203  filuni  24204  ufinffr  24248  alexsubALTlem2  24367  plyn0mulidp  26602  ellogdm  26967  nosepon  28022  noextenddif  28025  nomaxmo  28055  nosupinfsep  28089  nocvxminlem  28140  bdayfinbndlem1  28853  numedglnl  29722  lfuhgr3  29728  usgredg2v  29808  clwwlknon1nloop  30690  avril1  31064  shne0i  32050  chnlei  32087  cvnbtwn2  32889  cvnbtwn3  32890  cvnbtwn4  32891  chrelat2i  32967  atabs2i  33004  dmdbr5ati  33024  nmo  33086  disjdifprg  33169  eliccelico  33369  elicoelioo  33370  xrdifh  33372  f1ocnt  33392  tosglblem  33535  xrnarchi  33745  elrgspnlem2  33804  fldextrspunlsplem  34305  hasheuni  34717  cntnevol  34861  sitgaddlemb  34980  eulerpartlemgs2  35012  ballotlem2  35121  ballotlemodife  35130  bnj1143  35420  bnj1304  35449  bnj1476  35477  bnj1533  35482  bnj1174  35633  bnj1204  35642  bnj1280  35650  nummin  35722  axreg  35795  axregscl  35796  noinfepregs  35801  axregs  35807  kardexen  35831  vonf1wev  35887  vonf1owevOLD  35889  erdszelem9  35964  fmla0disjsuc  36163  dftr6  36516  fundmpss  36532  dfon2lem5  36549  dfon2lem8  36552  dfon2lem9  36553  wzel  36586  elfuns  36677  dfrecs2  36714  dffr7  36720  df3nandALT1  37187  andnand1  37189  imnand2  37190  regsfromregtco  37326  regsfromunir1  37328  bj-notalbii  37499  difunieq  38297  domalom  38327  fvineqsneq  38335  fdc  38679  nninfnub  38685  tsbi4  39068  ts3an2  39083  ts3an3  39084  ts3or1  39085  vvdifopab  39197  brvvdif  39200  n0elqs  39264  dfssr2  39511  lcvnbtwn2  40084  lcvnbtwn3  40085  cvrnbtwn3  40333  dalem18  40738  lhpocnel2  41076  cdleme0nex  41347  cdlemk19w  42029  dihglblem6  42397  dvh2dim  42502  dvh3dim3N  42506  aks4d1p7  43133  aks6d1c5  43189  sticksstones1  43196  aks6d1c6lem3  43222  redvmptabs  43411  ctbnfien  43824  rencldnfilem  43826  numinfctb  44104  onmaxnelsup  44224  onsupnmax  44229  onsupuni  44230  onsupeqnmax  44248  oenassex  44319  naddgeoa  44395  ifpnorcor  44480  ifpnancor  44481  ifpdfnan  44486  ifpananb  44506  ifpnannanb  44507  ifpxorxorb  44511  rp-isfinite6  44518  pwinfig  44561  elnonrel  44585  iunrelexp0  44701  frege131  44993  frege133  44995  compab  45424  zfregs2VD  45822  undif3VD  45863  sineq0ALT  45918  rext0  45920  permac8prim  46003  ndisj2  46067  ralfal  46175  uz0  46421  icccncfext  46896  itgioocnicc  46986  fourierdlem42  47158  fourierdlem62  47177  fourierdlem93  47208  fourierdlem101  47216  nsssmfmbf  47788  aiotavb  48159  afv2ndeffv0  48329  otiunsndisjX  48348  nltle2tri  48382  0nelsetpreimafv  48471  evennodd  48740