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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  sylnbi  333  xchnxbi  335  xchbinx  337  oplem1  1056  xorcomOLD  1510  xorbi12iOLD  1521  norcomOLD  1528  noranOLD  1532  nororOLD  1534  norassOLD  1539  nic-axALT  1681  tbw-bijust  1705  rb-bijust  1756  19.43OLD  1890  cbvexvw  2049  hbn1fw  2057  hba1w  2059  excom  2170  cbvexv1  2345  cbvex2v  2348  cbvrexfw  3338  cbvrexf  3340  cgsex4g  3443  cbvrexcsf  3834  dfss4  4150  indifdirOLD  4177  neq0f  4231  n0el  4251  ab0ALT  4266  ab0orv  4268  abn0  4270  pssdifcom2  4378  difprsnss  4688  brdif  5084  otiunsndisj  5378  difopab  5675  rexiunxp  5684  rexxpf  5691  rnep  5771  somin1  5968  cnvdif  5977  difxp  5997  imadif  6424  brprcneu  6668  fvprc  6669  dffv2  6766  ovima0  7346  porpss  7474  tfinds  7596  poxp  7851  tz7.48lem  8109  brsdom  8581  brsdom2  8694  unfi  8774  fimax2g  8841  ordunifi  8845  dfsup2  8984  supgtoreq  9010  infcllem  9027  suc11reg  9158  rankxplim2  9385  rankxplim3  9386  alephval3  9613  kmlem4  9656  cflim2  9766  isfin4-2  9817  fin23lem25  9827  fin1a2lem5  9907  fin12  9916  axcclem  9960  zorng  10007  infinf  10069  alephadd  10080  fpwwe2  10146  axpre-lttri  10668  dfinfre  11702  infrenegsup  11704  arch  11976  rpneg  12507  xmulcom  12745  xmulneg1  12748  xmulf  12751  xrinfmss2  12790  difreicc  12961  fzp1nel  13085  ssnn0fi  13447  fsuppmapnn0fiubex  13454  hashfun  13893  swrdccatin2  14183  s3iunsndisj  14420  incexc2  15289  lcmftp  16080  f1omvdco3  18698  psgnunilem4  18746  gsumcom3  19220  gsumxp2  19222  0ringnnzr  20164  mdetunilem7  21372  fctop  21758  cctop  21760  ntreq0  21831  ordtbas2  21945  cmpcld  22156  hausdiag  22399  fbun  22594  fbfinnfr  22595  opnfbas  22596  fbasrn  22638  filuni  22639  ufinffr  22683  alexsubALTlem2  22802  ellogdm  25385  numedglnl  27092  usgredg2v  27172  clwwlknon1nloop  28039  avril1  28403  shne0i  29386  chnlei  29423  cvnbtwn2  30225  cvnbtwn3  30226  cvnbtwn4  30227  chrelat2i  30303  atabs2i  30340  dmdbr5ati  30360  nelbOLD  30394  nmo  30415  disjdifprg  30491  eliccelico  30676  elicoelioo  30677  xrdifh  30679  f1ocnt  30701  tosglblem  30832  xrnarchi  31018  hasheuni  31626  cntnevol  31769  sitgaddlemb  31888  eulerpartlemgs2  31920  ballotlem2  32028  ballotlemodife  32037  plymulx0  32099  bnj1143  32344  bnj1304  32373  bnj1476  32401  bnj1533  32406  bnj1174  32557  bnj1204  32566  bnj1280  32574  nummin  32637  0nn0m1nnn0  32645  lfuhgr3  32655  erdszelem9  32735  fmla0disjsuc  32934  dftr6  33294  fundmpss  33317  dfon2lem5  33340  dfon2lem8  33343  dfon2lem9  33344  xpord2pred  33408  xpord2ind  33410  wzel  33434  nosepon  33514  noextenddif  33517  nomaxmo  33547  nosupinfsep  33581  nocvxminlem  33618  elfuns  33863  dfrecs2  33898  df3nandALT1  34234  andnand1  34236  imnand2  34237  bj-notalbii  34442  difunieq  35191  domalom  35221  fvineqsneq  35229  fdc  35549  nninfnub  35555  tsbi4  35940  ts3an2  35955  ts3an3  35956  ts3or1  35957  vvdifopab  36045  brvvdif  36048  n0elqs  36107  dfssr2  36263  lcvnbtwn2  36687  lcvnbtwn3  36688  cvrnbtwn3  36936  dalem18  37341  lhpocnel2  37679  cdleme0nex  37950  cdlemk19w  38632  dihglblem6  39000  dvh2dim  39105  dvh3dim3N  39109  sticksstones1  39731  metakunt1  39739  ctbnfien  40235  rencldnfilem  40237  numinfctb  40523  ifpnorcor  40664  ifpnancor  40665  ifpdfnan  40670  ifpananb  40690  ifpnannanb  40691  ifpxorxorb  40695  rp-isfinite6  40702  pwinfig  40736  elnonrel  40761  iunrelexp0  40879  frege131  41171  frege133  41173  compab  41621  zfregs2VD  42022  undif3VD  42063  sineq0ALT  42118  ndisj2  42160  uz0  42513  icccncfext  42993  itgioocnicc  43083  fourierdlem42  43255  fourierdlem62  43274  fourierdlem93  43305  fourierdlem101  43313  nsssmfmbf  43876  aiotavb  44144  afv2ndeffv0  44315  otiunsndisjX  44334  nltle2tri  44369  0nelsetpreimafv  44406  evennodd  44659