Theorem notbii 319

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  sylnbi  329  xchnxbi  331  xchbinx  333  oplem1  1053  xorcomOLD  1507  xorbi12iOLD  1518  norcomOLD  1525  noranOLD  1529  nororOLD  1531  norassOLD  1536  nic-axALT  1678  tbw-bijust  1702  rb-bijust  1753  19.43OLD  1887  cbvexvw  2041  hbn1fw  2049  hba1w  2051  exexw  2055  excom  2164  cbvrexfw  3360  cbvrexf  3362  cgsex4g  3466  cbvrexcsf  3874  dfss4  4189  indifdirOLD  4216  neq0f  4272  n0el  4292  ab0ALT  4307  ab0orv  4309  abn0  4311  pssdifcom2  4418  difprsnss  4729  brdif  5123  otiunsndisj  5428  difopab  5729  rexiunxp  5738  rexxpf  5745  rnep  5825  somin1  6027  cnvdif  6036  difxp  6056  imadif  6502  brprcneu  6747  fvprc  6748  dffv2  6845  ovima0  7429  porpss  7558  tfinds  7681  poxp  7940  tz7.48lem  8242  brsdom  8718  brsdom2  8837  unfi  8917  fimax2g  8990  ordunifi  8994  dfsup2  9133  supgtoreq  9159  infcllem  9176  suc11reg  9307  rankxplim2  9569  rankxplim3  9570  alephval3  9797  kmlem4  9840  cflim2  9950  isfin4-2  10001  fin23lem25  10011  fin1a2lem5  10091  fin12  10100  axcclem  10144  zorng  10191  infinf  10253  alephadd  10264  fpwwe2  10330  axpre-lttri  10852  dfinfre  11886  infrenegsup  11888  arch  12160  rpneg  12691  xmulcom  12929  xmulneg1  12932  xmulf  12935  xrinfmss2  12974  difreicc  13145  fzp1nel  13269  ssnn0fi  13633  fsuppmapnn0fiubex  13640  hashfun  14080  swrdccatin2  14370  s3iunsndisj  14607  incexc2  15478  lcmftp  16269  f1omvdco3  18972  psgnunilem4  19020  gsumcom3  19494  gsumxp2  19496  0ringnnzr  20453  mdetunilem7  21675  fctop  22062  cctop  22064  ntreq0  22136  ordtbas2  22250  cmpcld  22461  hausdiag  22704  fbun  22899  fbfinnfr  22900  opnfbas  22901  fbasrn  22943  filuni  22944  ufinffr  22988  alexsubALTlem2  23107  ellogdm  25699  numedglnl  27417  usgredg2v  27497  clwwlknon1nloop  28364  avril1  28728  shne0i  29711  chnlei  29748  cvnbtwn2  30550  cvnbtwn3  30551  cvnbtwn4  30552  chrelat2i  30628  atabs2i  30665  dmdbr5ati  30685  nelbOLDOLD  30718  nmo  30739  disjdifprg  30815  eliccelico  31000  elicoelioo  31001  xrdifh  31003  f1ocnt  31025  tosglblem  31154  xrnarchi  31340  hasheuni  31953  cntnevol  32096  sitgaddlemb  32215  eulerpartlemgs2  32247  ballotlem2  32355  ballotlemodife  32364  plymulx0  32426  bnj1143  32670  bnj1304  32699  bnj1476  32727  bnj1533  32732  bnj1174  32883  bnj1204  32892  bnj1280  32900  nummin  32963  0nn0m1nnn0  32971  lfuhgr3  32981  erdszelem9  33061  fmla0disjsuc  33260  dftr6  33624  fundmpss  33646  dfon2lem5  33669  dfon2lem8  33672  dfon2lem9  33673  xpord2pred  33719  xpord2ind  33721  wzel  33745  nosepon  33795  noextenddif  33798  nomaxmo  33828  nosupinfsep  33862  nocvxminlem  33899  elfuns  34144  dfrecs2  34179  df3nandALT1  34515  andnand1  34517  imnand2  34518  bj-notalbii  34723  difunieq  35472  domalom  35502  fvineqsneq  35510  fdc  35830  nninfnub  35836  tsbi4  36221  ts3an2  36236  ts3an3  36237  ts3or1  36238  vvdifopab  36326  brvvdif  36329  n0elqs  36388  dfssr2  36544  lcvnbtwn2  36968  lcvnbtwn3  36969  cvrnbtwn3  37217  dalem18  37622  lhpocnel2  37960  cdleme0nex  38231  cdlemk19w  38913  dihglblem6  39281  dvh2dim  39386  dvh3dim3N  39390  aks4d1p7  40019  sticksstones1  40030  metakunt1  40053  ctbnfien  40556  rencldnfilem  40558  numinfctb  40844  ifpnorcor  40985  ifpnancor  40986  ifpdfnan  40991  ifpananb  41011  ifpnannanb  41012  ifpxorxorb  41016  rp-isfinite6  41023  pwinfig  41057  elnonrel  41082  iunrelexp0  41199  frege131  41491  frege133  41493  compab  41949  zfregs2VD  42350  undif3VD  42391  sineq0ALT  42446  ndisj2  42488  uz0  42842  icccncfext  43318  itgioocnicc  43408  fourierdlem42  43580  fourierdlem62  43599  fourierdlem93  43630  fourierdlem101  43638  nsssmfmbf  44201  aiotavb  44469  afv2ndeffv0  44639  otiunsndisjX  44658  nltle2tri  44693  0nelsetpreimafv  44730  evennodd  44983