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  1052  xorcomOLD  1506  xorbi12iOLD  1517  norcomOLD  1524  noranOLD  1528  nororOLD  1530  norassOLD  1535  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  19.43OLD  1884  cbvexvw  2044  hbn1fw  2052  hba1w  2054  excom  2166  cbvexv1  2351  cbvex2v  2354  cbvrexfw  3384  cbvrexf  3386  cgsex4g  3486  cbvrexcsf  3871  dfss4  4185  indifdir  4210  neq0f  4256  n0el  4275  ab0  4287  pssdifcom2  4394  difprsnss  4692  brdif  5083  otiunsndisj  5375  difopab  5666  rexiunxp  5675  rexxpf  5682  rnep  5761  somin1  5960  cnvdif  5969  difxp  5988  imadif  6408  brprcneu  6637  dffv2  6733  ovima0  7307  porpss  7433  tfinds  7554  poxp  7805  tz7.48lem  8060  brsdom  8515  brsdom2  8625  fimax2g  8748  ordunifi  8752  dfsup2  8892  supgtoreq  8918  infcllem  8935  suc11reg  9066  rankxplim2  9293  rankxplim3  9294  alephval3  9521  kmlem4  9564  cflim2  9674  isfin4-2  9725  fin23lem25  9735  fin1a2lem5  9815  fin12  9824  axcclem  9868  zorng  9915  infinf  9977  alephadd  9988  fpwwe2  10054  axpre-lttri  10576  dfinfre  11609  infrenegsup  11611  arch  11882  rpneg  12409  xmulcom  12647  xmulneg1  12650  xmulf  12653  xrinfmss2  12692  difreicc  12862  fzp1nel  12986  ssnn0fi  13348  fsuppmapnn0fiubex  13355  hashfun  13794  swrdccatin2  14082  s3iunsndisj  14319  incexc2  15185  lcmftp  15970  f1omvdco3  18569  psgnunilem4  18617  gsumcom3  19091  gsumxp2  19093  0ringnnzr  20035  mdetunilem7  21223  fctop  21609  cctop  21611  ntreq0  21682  ordtbas2  21796  cmpcld  22007  hausdiag  22250  fbun  22445  fbfinnfr  22446  opnfbas  22447  fbasrn  22489  filuni  22490  ufinffr  22534  alexsubALTlem2  22653  ellogdm  25230  numedglnl  26937  usgredg2v  27017  clwwlknon1nloop  27884  avril1  28248  shne0i  29231  chnlei  29268  cvnbtwn2  30070  cvnbtwn3  30071  cvnbtwn4  30072  chrelat2i  30148  atabs2i  30185  dmdbr5ati  30205  nelbOLD  30239  nmo  30261  disjdifprg  30338  eliccelico  30526  elicoelioo  30527  xrdifh  30529  f1ocnt  30551  tosglblem  30682  xrnarchi  30863  hasheuni  31454  cntnevol  31597  sitgaddlemb  31716  eulerpartlemgs2  31748  ballotlem2  31856  ballotlemodife  31865  plymulx0  31927  bnj1143  32172  bnj1304  32201  bnj1476  32229  bnj1533  32234  bnj1174  32385  bnj1204  32394  bnj1280  32402  0nn0m1nnn0  32461  nummin  32474  lfuhgr3  32479  erdszelem9  32559  fmla0disjsuc  32758  dftr6  33099  fundmpss  33122  dfon2lem5  33145  dfon2lem8  33148  dfon2lem9  33149  wzel  33224  nosepon  33285  noextenddif  33288  nomaxmo  33314  nocvxminlem  33360  elfuns  33489  dfrecs2  33524  df3nandALT1  33860  andnand1  33862  imnand2  33863  bj-notalbii  34061  difunieq  34791  domalom  34821  fvineqsneq  34829  wl-dfrexv  35014  wl-dfrexex  35015  fdc  35183  nninfnub  35189  tsbi4  35574  ts3an2  35589  ts3an3  35590  ts3or1  35591  vvdifopab  35681  brvvdif  35684  n0elqs  35743  dfssr2  35899  lcvnbtwn2  36323  lcvnbtwn3  36324  cvrnbtwn3  36572  dalem18  36977  lhpocnel2  37315  cdleme0nex  37586  cdlemk19w  38268  dihglblem6  38636  dvh2dim  38741  dvh3dim3N  38745  metakunt1  39350  ctbnfien  39759  rencldnfilem  39761  numinfctb  40047  ifpnorcor  40188  ifpnancor  40189  ifpdfnan  40194  ifpananb  40214  ifpnannanb  40215  ifpxorxorb  40219  rp-isfinite6  40226  pwinfig  40260  elnonrel  40285  iunrelexp0  40403  frege131  40695  frege133  40697  compab  41146  zfregs2VD  41547  undif3VD  41588  sineq0ALT  41643  ndisj2  41685  uz0  42049  icccncfext  42529  itgioocnicc  42619  fourierdlem42  42791  fourierdlem62  42810  fourierdlem93  42841  fourierdlem101  42849  nsssmfmbf  43412  aiotavb  43647  afv2ndeffv0  43816  otiunsndisjX  43835  nltle2tri  43870  0nelsetpreimafv  43907  evennodd  44161