Theorem neeq1 3022

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq1	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq1d 3019	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  pm13.18  3041  pm13.181  3042  nelrdva  3671  psseq1  4046  n0snor2el  4793  0inp0  5319  nnullss  5433  opeqex  5471  frsn  5739  xp11  6164  limeq  6361  tz6.12i  6897  fveqressseq  7064  funopsnOLD  7135  fprg  7142  tpres  7189  f1dom3el3dif  7257  f1ounsn  7260  f1prex  7272  isofrlem  7328  resf1extb  7919  f1oweALT  7957  frxp  8110  xpord2lem  8126  poxp2  8127  frxp2  8128  xpord2indlem  8131  xpord3lem  8133  frxp3  8135  xpord3inddlem  8138  suppimacnv  8158  elqsn0  8770  frfi  9233  fiint  9274  marypha1lem  9381  frmin  9709  eldju2ndl  9898  dfac8alem  10001  dfac8clem  10004  aceq3lem  10092  dfac5lem3  10097  dfac5lem4  10098  dfac5  10100  dfac2b  10102  dfac9  10108  kmlem1  10122  kmlem12  10133  kmlem14  10135  fin2i  10267  isfin2-2  10291  fin23lem21  10311  fin1a2lem10  10381  axcc2lem  10408  dominf  10417  ac5b  10450  zornn0g  10477  axdclem  10491  dominfac  10546  elwina  10659  elina  10660  iswun  10677  rankcf  10750  axrrecex  11136  elimne0  11184  1re  11196  recex  11834  xnn0nemnf  12576  uzn0  12867  qreccl  12981  xrnemnf  13130  xrnepnf  13131  xnn0n0n1ge2b  13145  fztpval  13602  expcl2lem  14097  hashnemnf  14368  hashneq0  14388  hashge2el2difr  14506  hashdmpropge2  14508  relexp1g  15051  ntrivcvgn0  15940  ntrivcvgmullem  15943  fprodntriv  15984  divalglem7  16445  divalg  16449  gcdcllem1  16545  gcdcllem3  16547  pcpre1  16890  pcqmul  16901  pcqcl  16904  prmgaplem3  17101  prmgaplem4  17102  xpsfrnel  17604  mreintcl  17635  isdrs  18345  isipodrs  18581  sgrp2rid2ex  18977  frgpuptinv  19829  isnzr2  20589  nrhmzr  20610  isdrngrd  20836  isdrngrdOLD  20838  isprmidl  21422  psgnodpmr  21697  lindfrn  21928  dmatelnd  22610  dmatmul  22611  mdetdiaglem  22712  mdetunilem1  22726  fvmptnn04ifa  22964  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  fiinopn  23015  hausnei  23442  dfconn2  23533  2ndcdisj  23570  regr1lem2  23854  isfbas  23943  ioorinv  25692  ioorcl  25693  vitalilem2  25725  vitalilem3  25726  vitali  25729  itg1climres  25830  mbfi1fseqlem4  25834  dvferm1lem  26100  dvferm2lem  26102  isuc1p  26255  ismon1p  26257  ply1remlem  26279  plydivlem4  26414  aannenlem1  26446  aannenlem2  26447  lgsne0  27453  lgsqr  27469  nolesgn2ores  27790  nogesgn1ores  27792  nosepdmlem  27801  nosupbnd1lem3  27828  nosupbnd1lem5  27830  nosupbnd2lem1  27833  noinfbnd1lem3  27843  noinfbnd1lem5  27845  noinfbnd2lem1  27848  axtg5seg  28688  axtgupdim2  28694  axtgeucl  28695  axlowdim1  29214  lpvtx  29323  umgrnloopv  29361  usgrnloopvALT  29456  umgrvad2edg  29468  cusgrfilem2  29711  pthdlem2lem  30021  iswwlks  30090  iswwlksnx  30094  2pthdlem1  30184  isclwwlk  30240  3pthdlem1  30420  upgr3v3e3cycl  30436  upgr4cycl4dv4e  30441  eupth2lem2  30475  eupth2lem3lem4  30487  eupth2lem3lem6  30489  3cyclfrgrrn1  30541  4cycl2vnunb  30546  frgrreg  30650  norm1exi  31507  shintcl  31587  chintcl  31589  chne0  31751  elspansn2  31824  eigre  32092  eigorth  32095  kbpj  32213  superpos  32611  hatomic  32617  ismxidl  33657  ssmxidllem  33668  ssmxidl  33669  constrconj  34047  constrcccllem  34056  constrcbvlem  34057  2sqr3minply  34082  zarcmplem  34183  xrge0iifhom  34239  xrge0iif1  34240  esumpr2  34369  sibfof  34642  signswn0  34859  signswch  34860  signstfvneq0  34871  axtgupdim2ALTV  34967  bnj168  35031  bnj970  35247  bnj1154  35299  onvf1odlem2  35454  umgracycusgr  35512  cusgracyclt3v  35514  subfacp1lem1  35537  erdszelem8  35556  indispconn  35592  cvmsss2  35632  nepss  36076  elwlim  36179  dfrdg4  36309  fvray  36499  linedegen  36501  fvline  36502  hilbert1.1  36512  rankeq1o  36529  unblimceq0lem  36952  knoppndvlem21  36978  qdiff  37826  poimirlem1  38127  poimirlem17  38143  poimirlem20  38146  poimirlem32  38158  itg2addnclem3  38179  neificl  38259  isdrngo3  38465  ispridl  38540  ismaxidl  38546  islshp  39610  lsatn0  39630  lshpset2N  39750  atlex  39947  hlsuprexch  40012  3dimlem1  40089  llni2  40143  lplni2  40168  2llnjN  40198  lvoli2  40212  2lplnj  40251  islinei  40371  lnatexN  40410  llnexchb2  40500  lhpmatb  40662  cdleme40m  41098  cdlemftr3  41196  cdlemk28-3  41539  cdlemk35s  41568  cdlemk39s  41570  cdlemk42  41572  nnn1suc  42888  dnnumch1  43628  aomclem3  43640  aomclem8  43645  dfac11  43646  dfacbasgrp  43692  dfsucon  44106  ax6e2ndeq  45127  ax6e2ndeqVD  45476  relpfrlem  45521  permac8prim  45582  fnchoice  45608  fiiuncl  45644  disjrnmpt2  45765  idlimc  46201  limcperiod  46203  limclner  46224  cnrefiisp  46403  climxlim2lem  46418  fperdvper  46492  stoweidlem35  46608  stoweidlem43  46616  stoweidlem59  46632  fourierdlem76  46755  etransclem47  46854  nnfoctbdjlem  47028  elprneb  47622  ichexmpl1  48074  ichnreuop  48077  vopnbgrel  48475  dfclnbgr6  48477  dfnbgr6  48478  usgrgrtrirex  48571  isubgr3stgrlem4  48590  usgrexmpl2trifr  48658  gpg3kgrtriex  48710  itcoval2  49296  itcoval3  49297  itcovalsuc  49299  ackvalsuc1mpt  49310  inlinecirc02plem  49418  oppcthinendcALT  50071