Theorem notbii 321

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  sylnbi  331  xchnxbi  333  xchbinx  335  oplem1  1062  nic-axALT  1681  tbw-bijust  1705  rb-bijust  1756  19.43OLD  1890  cbvexvw  2044  hbn1fw  2054  hba1w  2056  exexw  2060  excom  2173  cbvrexf  3325  cbvrexcsf  3874  dfss4  4197  neq0f  4276  n0el  4292  ab0ALT  4309  abn0  4313  pssdifcom2  4418  difprsnss  4732  brdif  5125  otthne  5426  otiunsndisj  5461  difopab  5773  rexiunxp  5782  rexxpf  5789  dm0rn0  5866  rnep  5869  somin1  6083  cnvdif  6094  difxp  6115  imadif  6569  brprcneu  6817  brprcneuALT  6818  dffv2  6922  ovima0  7535  porpss  7670  tfinds  7800  poxp  8068  xpord2pred  8085  xpord2indlem  8087  tz7.48lem  8370  brsdom  8911  brsdom2  9029  unfi  9095  fimax2g  9186  ordunifi  9190  dfsup2  9347  supgtoreq  9374  infcllem  9391  suc11reg  9531  rankxplim2  9795  rankxplim3  9796  alephval3  10023  kmlem4  10067  cflim2  10176  isfin4-2  10227  fin23lem25  10237  fin1a2lem5  10317  fin12  10326  axcclem  10370  zorng  10417  alephadd  10491  fpwwe2  10557  axpre-lttri  11079  dfinfre  12128  infrenegsup  12130  arch  12425  rpneg  12967  xmulcom  13209  xmulneg1  13212  xmulf  13215  xrinfmss2  13254  difreicc  13428  fzp1nel  13556  ssnn0fi  13938  fsuppmapnn0fiubex  13945  hashfun  14390  swrdccatin2  14682  s3iunsndisj  14921  incexc2  15794  lcmftp  16596  f1omvdco3  19415  psgnunilem4  19463  gsumcom3  19944  gsumxp2  19946  0ringnnzr  20497  mdetunilem7  22601  fctop  22987  cctop  22989  ntreq0  23060  ordtbas2  23174  cmpcld  23385  hausdiag  23628  fbun  23823  fbfinnfr  23824  opnfbas  23825  fbasrn  23867  filuni  23868  ufinffr  23912  alexsubALTlem2  24031  ellogdm  26621  nosepon  27647  noextenddif  27650  nomaxmo  27680  nosupinfsep  27714  nocvxminlem  27764  bdayfinbndlem1  28477  numedglnl  29231  usgredg2v  29314  clwwlknon1nloop  30187  avril1  30551  shne0i  31537  chnlei  31574  cvnbtwn2  32376  cvnbtwn3  32377  cvnbtwn4  32378  chrelat2i  32454  atabs2i  32491  dmdbr5ati  32511  nmo  32577  disjdifprg  32664  eliccelico  32869  elicoelioo  32870  xrdifh  32872  f1ocnt  32892  tosglblem  33053  xrnarchi  33265  elrgspnlem2  33324  fldextrspunlsplem  33857  hasheuni  34269  cntnevol  34412  sitgaddlemb  34532  eulerpartlemgs2  34564  ballotlem2  34673  ballotlemodife  34682  plymulx0  34731  bnj1143  34972  bnj1304  35001  bnj1476  35029  bnj1533  35034  bnj1174  35185  bnj1204  35194  bnj1280  35202  nummin  35274  axreg  35308  axregscl  35309  noinfepregs  35314  axregs  35320  vonf1owev  35336  0nn0m1nnn0  35341  lfuhgr3  35348  erdszelem9  35427  fmla0disjsuc  35626  dftr6  35979  fundmpss  35995  dfon2lem5  36013  dfon2lem8  36016  dfon2lem9  36017  wzel  36050  elfuns  36141  dfrecs2  36178  df3nandALT1  36627  andnand1  36629  imnand2  36630  regsfromregtco  36766  regsfromunir1  36768  bj-notalbii  36940  difunieq  37736  domalom  37766  fvineqsneq  37774  fdc  38112  nninfnub  38118  tsbi4  38503  ts3an2  38518  ts3an3  38519  ts3or1  38520  vvdifopab  38632  brvvdif  38635  n0elqs  38699  dfssr2  38946  lcvnbtwn2  39519  lcvnbtwn3  39520  cvrnbtwn3  39768  dalem18  40173  lhpocnel2  40511  cdleme0nex  40782  cdlemk19w  41464  dihglblem6  41832  dvh2dim  41937  dvh3dim3N  41941  aks4d1p7  42568  aks6d1c5  42624  sticksstones1  42631  aks6d1c6lem3  42657  redvmptabs  42837  ctbnfien  43263  rencldnfilem  43265  numinfctb  43548  onmaxnelsup  43668  onsupnmax  43673  onsupuni  43674  onsupeqnmax  43692  oenassex  43763  naddgeoa  43839  ifpnorcor  43924  ifpnancor  43925  ifpdfnan  43930  ifpananb  43950  ifpnannanb  43951  ifpxorxorb  43955  rp-isfinite6  43962  pwinfig  44005  elnonrel  44029  iunrelexp0  44146  frege131  44438  frege133  44440  compab  44885  zfregs2VD  45284  undif3VD  45325  sineq0ALT  45380  rext0  45382  permac8prim  45458  ndisj2  45499  ralfal  45608  uz0  45855  icccncfext  46330  itgioocnicc  46420  fourierdlem42  46592  fourierdlem62  46611  fourierdlem93  46642  fourierdlem101  46650  nsssmfmbf  47222  aiotavb  47553  afv2ndeffv0  47723  otiunsndisjX  47742  nltle2tri  47776  0nelsetpreimafv  47865  evennodd  48134