Theorem notbii 320

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  sylnbi  330  xchnxbi  332  xchbinx  334  oplem1  1056  nic-axALT  1673  tbw-bijust  1697  rb-bijust  1748  19.43OLD  1882  cbvexvw  2035  hbn1fw  2044  hba1w  2046  exexw  2050  excom  2161  cbvrexf  3338  cgsex4gOLD  3506  cbvrexcsf  3915  dfss4  4242  neq0f  4321  n0el  4337  ab0ALT  4354  ab0orv  4356  abn0  4358  pssdifcom2  4464  difprsnss  4772  brdif  5169  otthne  5458  otiunsndisj  5492  difopab  5806  difopabOLD  5807  rexiunxp  5817  rexxpf  5824  rnep  5903  somin1  6119  cnvdif  6129  difxp  6150  imadif  6616  brprcneu  6862  brprcneuALT  6863  dffv2  6970  ovima0  7580  porpss  7715  tfinds  7849  poxp  8121  xpord2pred  8138  xpord2indlem  8140  tz7.48lem  8449  brsdom  8983  brsdom2  9105  unfi  9179  fimax2g  9288  ordunifi  9292  dfsup2  9450  supgtoreq  9476  infcllem  9493  suc11reg  9625  rankxplim2  9886  rankxplim3  9887  alephval3  10116  kmlem4  10160  cflim2  10269  isfin4-2  10320  fin23lem25  10330  fin1a2lem5  10410  fin12  10419  axcclem  10463  zorng  10510  infinf  10572  alephadd  10583  fpwwe2  10649  axpre-lttri  11171  dfinfre  12215  infrenegsup  12217  arch  12490  rpneg  13033  xmulcom  13274  xmulneg1  13277  xmulf  13280  xrinfmss2  13319  difreicc  13490  fzp1nel  13617  ssnn0fi  13992  fsuppmapnn0fiubex  13999  hashfun  14443  swrdccatin2  14734  s3iunsndisj  14974  incexc2  15841  lcmftp  16640  f1omvdco3  19415  psgnunilem4  19463  gsumcom3  19944  gsumxp2  19946  0ringnnzr  20470  mdetunilem7  22541  fctop  22927  cctop  22929  ntreq0  23000  ordtbas2  23114  cmpcld  23325  hausdiag  23568  fbun  23763  fbfinnfr  23764  opnfbas  23765  fbasrn  23807  filuni  23808  ufinffr  23852  alexsubALTlem2  23971  ellogdm  26584  nosepon  27613  noextenddif  27616  nomaxmo  27646  nosupinfsep  27680  nocvxminlem  27725  numedglnl  29055  usgredg2v  29138  clwwlknon1nloop  30012  avril1  30376  shne0i  31361  chnlei  31398  cvnbtwn2  32200  cvnbtwn3  32201  cvnbtwn4  32202  chrelat2i  32278  atabs2i  32315  dmdbr5ati  32335  nmo  32403  disjdifprg  32489  eliccelico  32688  elicoelioo  32689  xrdifh  32691  f1ocnt  32713  tosglblem  32873  xrnarchi  33100  elrgspnlem2  33156  fldextrspunlsplem  33630  hasheuni  34024  cntnevol  34167  sitgaddlemb  34288  eulerpartlemgs2  34320  ballotlem2  34429  ballotlemodife  34438  plymulx0  34500  bnj1143  34742  bnj1304  34771  bnj1476  34799  bnj1533  34804  bnj1174  34955  bnj1204  34964  bnj1280  34972  nummin  35043  0nn0m1nnn0  35056  lfuhgr3  35063  erdszelem9  35142  fmla0disjsuc  35341  dftr6  35689  fundmpss  35705  dfon2lem5  35726  dfon2lem8  35729  dfon2lem9  35730  wzel  35763  elfuns  35854  dfrecs2  35889  df3nandALT1  36338  andnand1  36340  imnand2  36341  bj-notalbii  36553  difunieq  37313  domalom  37343  fvineqsneq  37351  fdc  37690  nninfnub  37696  tsbi4  38081  ts3an2  38096  ts3an3  38097  ts3or1  38098  vvdifopab  38199  brvvdif  38202  n0elqs  38265  dfssr2  38438  lcvnbtwn2  38966  lcvnbtwn3  38967  cvrnbtwn3  39215  dalem18  39621  lhpocnel2  39959  cdleme0nex  40230  cdlemk19w  40912  dihglblem6  41280  dvh2dim  41385  dvh3dim3N  41389  aks4d1p7  42018  aks6d1c5  42074  sticksstones1  42081  aks6d1c6lem3  42107  metakunt1  42140  redvmptabs  42328  sn-tz6.12-2  42628  ctbnfien  42766  rencldnfilem  42768  numinfctb  43052  onmaxnelsup  43172  onsupnmax  43177  onsupuni  43178  onsupeqnmax  43196  oenassex  43267  naddgeoa  43343  ifpnorcor  43429  ifpnancor  43430  ifpdfnan  43435  ifpananb  43455  ifpnannanb  43456  ifpxorxorb  43460  rp-isfinite6  43467  pwinfig  43510  elnonrel  43534  iunrelexp0  43651  frege131  43943  frege133  43945  compab  44392  zfregs2VD  44792  undif3VD  44833  sineq0ALT  44888  rext0  44890  ndisj2  45002  ralfal  45112  uz0  45367  icccncfext  45846  itgioocnicc  45936  fourierdlem42  46108  fourierdlem62  46127  fourierdlem93  46158  fourierdlem101  46166  nsssmfmbf  46738  aiotavb  47047  afv2ndeffv0  47217  otiunsndisjX  47236  nltle2tri  47270  0nelsetpreimafv  47322  evennodd  47575