Theorem neeq1 3018

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 3015	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  pm13.18  3037  pm13.181  3038  nelrdva  3663  psseq1  4038  n0snor2el  4793  0inp0  5320  nnullss  5430  opeqex  5470  frsn  5739  xp11  6166  limeq  6367  tz6.12i  6903  fveqressseq  7071  funopsnOLD  7144  fprg  7151  tpres  7199  f1dom3el3dif  7265  f1ounsn  7272  f1prex  7284  isofrlem  7340  resf1extb  7935  f1oweALT  7973  frxp  8127  xpord2lem  8143  poxp2  8144  frxp2  8145  xpord2indlem  8148  xpord3lem  8150  frxp3  8152  xpord3inddlem  8155  suppimacnv  8175  elqsn0  8789  frfi  9260  fiint  9302  marypha1lem  9409  frmin  9737  eldju2ndl  9986  dfac8alem  10089  dfac8clem  10092  aceq3lem  10180  dfac5lem3  10185  dfac5lem4  10186  dfac5  10188  dfac2b  10190  dfac9  10196  kmlem1  10210  kmlem12  10221  kmlem14  10223  fin2i  10354  isfin2-2  10378  fin23lem21  10398  fin1a2lem10  10468  axcc2lem  10495  dominf  10504  ac5b  10537  zornn0g  10564  axdclem  10578  dominfac  10639  elwina  10752  elina  10753  iswun  10770  rankcf  10843  axrrecex  11229  elimne0  11277  1re  11289  recex  11929  xnn0nemnf  12671  uzn0  12963  qreccl  13078  xrnemnf  13227  xrnepnf  13228  xnn0n0n1ge2b  13242  fztpval  13700  expcl2lem  14196  hashnemnf  14468  hashneq0  14488  hashge2el2difr  14606  hashdmpropge2  14608  relexp1g  15159  ntrivcvgn0  16047  ntrivcvgmullem  16050  fprodntriv  16089  divalglem7  16549  divalg  16553  gcdcllem1  16649  gcdcllem3  16651  pcpre1  17000  pcqmul  17011  pcqcl  17014  prmgaplem3  17211  prmgaplem4  17212  xpsfrnel  17714  mreintcl  17745  isdrs  18455  isipodrs  18691  sgrp2rid2ex  19106  frgpuptinv  19965  isnzr2  20748  nrhmzr  20769  isdrng5  20988  isdrngrd  21003  isdrngrdOLD  21005  isprmidl  21599  psgnodpmr  21876  lindfrn  22107  dmatelnd  22791  dmatmul  22792  mdetdiaglem  22893  mdetunilem1  22907  fvmptnn04ifa  23148  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  fiinopn  23199  hausnei  23626  dfconn2  23717  2ndcdisj  23755  regr1lem2  24039  isfbas  24128  ioorinv  25877  ioorcl  25878  vitalilem2  25910  vitalilem3  25911  vitali  25914  itg1climres  26015  mbfi1fseqlem4  26019  dvferm1lem  26284  dvferm2lem  26286  isuc1p  26439  ismon1p  26441  ply1remlem  26463  plydivlem4  26599  aannenlem1  26637  aannenlem2  26638  lgsne0  27644  lgsqr  27660  nolesgn2ores  28011  nogesgn1ores  28013  nosepdmlem  28022  nosupbnd1lem3  28049  nosupbnd1lem5  28051  nosupbnd2lem1  28054  noinfbnd1lem3  28064  noinfbnd1lem5  28066  noinfbnd2lem1  28069  axtg5seg  28909  axtgupdim2  28915  axtgeucl  28916  elcgrabasi  29357  axlowdim1  29519  lpvtx  29628  umgrnloopv  29666  usgrnloopvALT  29764  umgrvad2edg  29776  cusgrfilem2  30019  pthdlem2lem  30335  iswwlks  30407  iswwlksnx  30411  2pthdlem1  30501  isclwwlk  30557  3pthdlem1  30747  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eupth2lem2  30802  eupth2lem3lem4  30814  eupth2lem3lem6  30816  3cyclfrgrrn1  30868  4cycl2vnunb  30873  frgrreg  30977  norm1exi  31834  shintcl  31914  chintcl  31916  chne0  32078  elspansn2  32151  eigre  32419  eigorth  32422  kbpj  32540  superpos  32938  hatomic  32944  ismxidl  33969  ssmxidllem  33980  ssmxidl  33981  constrconj  34359  constrcccllem  34368  constrcbvlem  34369  2sqr3minply  34394  zarcmplem  34495  xrge0iifhom  34551  xrge0iif1  34552  esumpr2  34681  sibfof  34955  signswn0  35172  signswch  35173  signstfvneq0  35184  axtgupdim2ALTV  35280  bnj168  35344  bnj970  35560  bnj1154  35612  onvf1odlem2  35856  umgracycusgr  35888  cusgracyclt3v  35890  subfacp1lem1  35913  erdszelem8  35932  indispconn  35968  cvmsss2  36008  nepss  36452  elwlim  36555  dfrdg4  36685  fvray  36876  linedegen  36878  fvline  36879  hilbert1.1  36889  rankeq1o  36902  unblimceq0lem  37342  knoppndvlem21  37368  qdiff  38216  poimirlem1  38507  poimirlem17  38523  poimirlem20  38526  poimirlem32  38538  itg2addnclem3  38559  neificl  38655  isdrngo3  38861  ispridl  38936  ismaxidl  38942  islshp  40004  lsatn0  40024  lshpset2N  40144  atlex  40341  hlsuprexch  40406  3dimlem1  40483  llni2  40537  lplni2  40562  2llnjN  40592  lvoli2  40606  2lplnj  40645  islinei  40765  lnatexN  40804  llnexchb2  40894  lhpmatb  41056  cdleme40m  41492  cdlemftr3  41590  cdlemk28-3  41933  cdlemk35s  41962  cdlemk39s  41964  cdlemk42  41966  nnn1suc  43299  dnnumch1  44004  aomclem3  44016  aomclem8  44021  dfac11  44022  dfacbasgrp  44068  dfsucon  44482  ax6e2ndeq  45501  ax6e2ndeqVD  45850  relpfrlem  45895  permac8prim  45956  fnchoice  45989  fiiuncl  46025  disjrnmpt2  46146  idlimc  46582  limcperiod  46584  limclner  46605  cnrefiisp  46784  climxlim2lem  46799  fperdvper  46873  stoweidlem35  46989  stoweidlem43  46997  stoweidlem59  47013  fourierdlem76  47136  etransclem47  47235  nnfoctbdjlem  47409  elprneb  48043  ichexmpl1  48495  ichnreuop  48498  vopnbgrel  48896  dfclnbgr6  48898  dfnbgr6  48899  usgrgrtrirex  48992  isubgr3stgrlem4  49011  usgrexmpl2trifr  49079  gpg3kgrtriex  49131  itcoval2  49720  itcoval3  49721  itcovalsuc  49723  ackvalsuc1mpt  49734  inlinecirc02plem  49842  oppcthinendcALT  50493  veronesev1lem  50917  veronesev2lem  50918  veronesev3lem  50919  veronesev4lem  50920  veronesev5lem  50921  veronesev6lem  50922  veronesevrowd  50923