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  1675  tbw-bijust  1699  rb-bijust  1750  19.43OLD  1884  cbvexvw  2038  hbn1fw  2048  hba1w  2050  exexw  2054  excom  2167  cbvrexf  3331  cgsex4gOLD  3488  cbvrexcsf  3892  dfss4  4221  neq0f  4300  n0el  4316  ab0ALT  4333  abn0  4337  pssdifcom2  4443  difprsnss  4755  brdif  5151  otthne  5434  otiunsndisj  5468  difopab  5779  rexiunxp  5789  rexxpf  5796  dm0rn0  5873  rnep  5876  somin1  6090  cnvdif  6101  difxp  6122  imadif  6576  brprcneu  6824  brprcneuALT  6825  dffv2  6929  ovima0  7537  porpss  7672  tfinds  7802  poxp  8070  xpord2pred  8087  xpord2indlem  8089  tz7.48lem  8372  brsdom  8911  brsdom2  9029  unfi  9095  fimax2g  9186  ordunifi  9190  dfsup2  9347  supgtoreq  9374  infcllem  9391  suc11reg  9528  rankxplim2  9792  rankxplim3  9793  alephval3  10020  kmlem4  10064  cflim2  10173  isfin4-2  10224  fin23lem25  10234  fin1a2lem5  10314  fin12  10323  axcclem  10367  zorng  10414  alephadd  10488  fpwwe2  10554  axpre-lttri  11076  dfinfre  12123  infrenegsup  12125  arch  12398  rpneg  12939  xmulcom  13181  xmulneg1  13184  xmulf  13187  xrinfmss2  13226  difreicc  13400  fzp1nel  13527  ssnn0fi  13908  fsuppmapnn0fiubex  13915  hashfun  14360  swrdccatin2  14652  s3iunsndisj  14891  incexc2  15761  lcmftp  16563  f1omvdco3  19378  psgnunilem4  19426  gsumcom3  19907  gsumxp2  19909  0ringnnzr  20458  mdetunilem7  22562  fctop  22948  cctop  22950  ntreq0  23021  ordtbas2  23135  cmpcld  23346  hausdiag  23589  fbun  23784  fbfinnfr  23785  opnfbas  23786  fbasrn  23828  filuni  23829  ufinffr  23873  alexsubALTlem2  23992  ellogdm  26604  nosepon  27633  noextenddif  27636  nomaxmo  27666  nosupinfsep  27700  nocvxminlem  27750  bdayfinbndlem1  28463  numedglnl  29217  usgredg2v  29300  clwwlknon1nloop  30174  avril1  30538  shne0i  31523  chnlei  31560  cvnbtwn2  32362  cvnbtwn3  32363  cvnbtwn4  32364  chrelat2i  32440  atabs2i  32477  dmdbr5ati  32497  nmo  32564  disjdifprg  32650  eliccelico  32857  elicoelioo  32858  xrdifh  32860  f1ocnt  32880  tosglblem  33056  xrnarchi  33266  elrgspnlem2  33325  fldextrspunlsplem  33830  hasheuni  34242  cntnevol  34385  sitgaddlemb  34505  eulerpartlemgs2  34537  ballotlem2  34646  ballotlemodife  34655  plymulx0  34704  bnj1143  34946  bnj1304  34975  bnj1476  35003  bnj1533  35008  bnj1174  35159  bnj1204  35168  bnj1280  35176  nummin  35249  axreg  35283  axregscl  35284  noinfepregs  35289  axregs  35295  vonf1owev  35302  0nn0m1nnn0  35307  lfuhgr3  35314  erdszelem9  35393  fmla0disjsuc  35592  dftr6  35945  fundmpss  35961  dfon2lem5  35979  dfon2lem8  35982  dfon2lem9  35983  wzel  36016  elfuns  36107  dfrecs2  36144  df3nandALT1  36593  andnand1  36595  imnand2  36596  regsfromregtr  36668  regsfromunir1  36670  bj-notalbii  36814  difunieq  37579  domalom  37609  fvineqsneq  37617  fdc  37946  nninfnub  37952  tsbi4  38337  ts3an2  38352  ts3an3  38353  ts3or1  38354  vvdifopab  38458  brvvdif  38461  n0elqs  38525  dfssr2  38752  lcvnbtwn2  39287  lcvnbtwn3  39288  cvrnbtwn3  39536  dalem18  39941  lhpocnel2  40279  cdleme0nex  40550  cdlemk19w  41232  dihglblem6  41600  dvh2dim  41705  dvh3dim3N  41709  aks4d1p7  42337  aks6d1c5  42393  sticksstones1  42400  aks6d1c6lem3  42426  redvmptabs  42615  ctbnfien  43060  rencldnfilem  43062  numinfctb  43345  onmaxnelsup  43465  onsupnmax  43470  onsupuni  43471  onsupeqnmax  43489  oenassex  43560  naddgeoa  43636  ifpnorcor  43721  ifpnancor  43722  ifpdfnan  43727  ifpananb  43747  ifpnannanb  43748  ifpxorxorb  43752  rp-isfinite6  43759  pwinfig  43802  elnonrel  43826  iunrelexp0  43943  frege131  44235  frege133  44237  compab  44682  zfregs2VD  45081  undif3VD  45122  sineq0ALT  45177  rext0  45179  permac8prim  45255  ndisj2  45296  ralfal  45405  uz0  45656  icccncfext  46131  itgioocnicc  46221  fourierdlem42  46393  fourierdlem62  46412  fourierdlem93  46443  fourierdlem101  46451  nsssmfmbf  47023  aiotavb  47336  afv2ndeffv0  47506  otiunsndisjX  47525  nltle2tri  47559  0nelsetpreimafv  47636  evennodd  47889