Theorem notbii 322

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  sylnbi  332  xchnxbi  334  xchbinx  336  oplem1  1068  nic-axALT  1694  tbw-bijust  1718  rb-bijust  1769  19.43OLD  1903  cbvexvw  2057  hbn1fw  2067  hba1w  2069  exexw  2073  excom  2196  cbvrexf  3348  cbvrexcsf  3895  dfss4  4221  neq0f  4300  n0el  4317  ab0ALT  4334  abn0  4338  pssdifcom2  4444  difprsnss  4759  brdif  5153  otthne  5454  otiunsndisj  5489  difopab  5803  rexiunxp  5812  rexxpf  5819  dm0rn0  5900  rnep  5903  somin1  6120  cnvdif  6127  difxp  6149  xpdifcnvepel  6154  imadif  6605  brprcneu  6857  brprcneuALT  6858  dffv2  6962  ovima0  7575  porpss  7710  tfinds  7840  poxp  8108  xpord2pred  8125  xpord2indlem  8127  tz7.48lem  8412  brsdom  8955  brsdom2  9073  unfi  9139  fimax2g  9230  ordunifi  9234  dfsup2  9390  supgtoreq  9417  infcllem  9434  suc11reg  9574  rankxplim2  9838  rankxplim3  9839  alephval3  10066  kmlem4  10110  cflim2  10220  isfin4-2  10271  fin23lem25  10281  fin1a2lem5  10361  fin12  10370  axcclem  10414  zorng  10461  alephadd  10535  fpwwe2  10601  axpre-lttri  11123  dfinfre  12173  infrenegsup  12175  arch  12478  rpneg  13027  xmulcom  13269  xmulneg1  13272  xmulf  13275  xrinfmss2  13314  difreicc  13488  fzp1nel  13616  ssnn0fi  13998  fsuppmapnn0fiubex  14005  hashfun  14450  swrdccatin2  14742  s3iunsndisj  14981  incexc2  15868  lcmftp  16670  f1omvdco3  19489  psgnunilem4  19537  gsumcom3  20018  gsumxp2  20020  0ringnnzr  20575  mdetunilem7  22678  fctop  23064  cctop  23066  ntreq0  23137  ordtbas2  23251  cmpcld  23462  hausdiag  23705  fbun  23900  fbfinnfr  23901  opnfbas  23902  fbasrn  23944  filuni  23945  ufinffr  23989  alexsubALTlem2  24108  plyn0mulidp  26345  ellogdm  26704  nosepon  27729  noextenddif  27732  nomaxmo  27762  nosupinfsep  27796  nocvxminlem  27847  bdayfinbndlem1  28560  numedglnl  29345  usgredg2v  29428  clwwlknon1nloop  30301  avril1  30665  shne0i  31651  chnlei  31688  cvnbtwn2  32490  cvnbtwn3  32491  cvnbtwn4  32492  chrelat2i  32568  atabs2i  32605  dmdbr5ati  32625  nmo  32689  disjdifprg  32775  eliccelico  32979  elicoelioo  32980  xrdifh  32982  f1ocnt  33002  tosglblem  33152  xrnarchi  33364  elrgspnlem2  33424  fldextrspunlsplem  33970  hasheuni  34382  cntnevol  34525  sitgaddlemb  34645  eulerpartlemgs2  34677  ballotlem2  34786  ballotlemodife  34795  bnj1143  35085  bnj1304  35114  bnj1476  35142  bnj1533  35147  bnj1174  35298  bnj1204  35307  bnj1280  35315  nummin  35389  axreg  35423  axregscl  35424  noinfepregs  35429  axregs  35435  vonf1wev  35451  vonf1owevOLD  35453  0nn0m1nnn0  35463  lfuhgr3  35470  erdszelem9  35549  fmla0disjsuc  35748  dftr6  36101  fundmpss  36117  dfon2lem5  36135  dfon2lem8  36138  dfon2lem9  36139  wzel  36172  elfuns  36263  dfrecs2  36300  df3nandALT1  36759  andnand1  36761  imnand2  36762  regsfromregtco  36898  regsfromunir1  36900  bj-notalbii  37072  difunieq  37868  domalom  37898  fvineqsneq  37906  fdc  38244  nninfnub  38250  tsbi4  38635  ts3an2  38650  ts3an3  38651  ts3or1  38652  vvdifopab  38764  brvvdif  38767  n0elqs  38831  dfssr2  39078  lcvnbtwn2  39651  lcvnbtwn3  39652  cvrnbtwn3  39900  dalem18  40305  lhpocnel2  40643  cdleme0nex  40914  cdlemk19w  41596  dihglblem6  41964  dvh2dim  42069  dvh3dim3N  42073  aks4d1p7  42700  aks6d1c5  42756  sticksstones1  42763  aks6d1c6lem3  42789  redvmptabs  42969  ctbnfien  43395  rencldnfilem  43397  numinfctb  43680  onmaxnelsup  43800  onsupnmax  43805  onsupuni  43806  onsupeqnmax  43824  oenassex  43895  naddgeoa  43971  ifpnorcor  44056  ifpnancor  44057  ifpdfnan  44062  ifpananb  44082  ifpnannanb  44083  ifpxorxorb  44087  rp-isfinite6  44094  pwinfig  44137  elnonrel  44161  iunrelexp0  44278  frege131  44570  frege133  44572  compab  45017  zfregs2VD  45416  undif3VD  45457  sineq0ALT  45512  rext0  45514  permac8prim  45590  ndisj2  45631  ralfal  45739  uz0  45986  icccncfext  46461  itgioocnicc  46551  fourierdlem42  46723  fourierdlem62  46742  fourierdlem93  46773  fourierdlem101  46781  nsssmfmbf  47353  aiotavb  47684  afv2ndeffv0  47854  otiunsndisjX  47873  nltle2tri  47907  0nelsetpreimafv  47996  evennodd  48265