Theorem neeq1 3017

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  pm13.18  3036  pm13.181  3037  nelrdva  3662  psseq1  4017  n0snor2el  4787  0inp0  5319  nnullss  5429  opeqex  5469  frsn  5738  xp11  6166  limeq  6374  tz6.12i  6912  fveqressseq  7080  funopsnOLD  7153  fprg  7160  tpres  7208  f1dom3el3dif  7274  f1ounsn  7281  f1prex  7293  isofrlem  7349  resf1extb  7947  f1oweALT  7985  frxp  8141  xpord2lem  8162  poxp2  8163  frxp2  8164  xpord2indlem  8167  xpord3lem  8169  frxp3  8171  xpord3inddlem  8174  suppimacnv  8195  elqsn0  8809  frfi  9280  fiint  9322  marypha1lem  9429  frmin  9757  eldju2ndl  10009  dfac8alem  10112  dfac8clem  10115  aceq3lem  10203  dfac5lem3  10208  dfac5lem4  10209  dfac5  10211  dfac2b  10213  dfac9  10219  kmlem1  10233  kmlem12  10244  kmlem14  10246  fin2i  10377  isfin2-2  10401  fin23lem21  10421  fin1a2lem10  10491  axcc2lem  10518  dominf  10527  ac5b  10560  zornn0g  10587  axdclem  10601  dominfac  10662  elwina  10775  elina  10776  iswun  10793  rankcf  10866  axrrecex  11252  elimne0  11300  1re  11312  recex  11952  xnn0nemnf  12694  uzn0  12986  qreccl  13101  xrnemnf  13250  xrnepnf  13251  xnn0n0n1ge2b  13265  fztpval  13724  expcl2lem  14220  hashnemnf  14492  hashneq0  14512  hashge2el2difr  14630  hashdmpropge2  14632  relexp1g  15185  ntrivcvgn0  16073  ntrivcvgmullem  16076  fprodntriv  16115  divalglem7  16575  divalg  16579  gcdcllem1  16675  gcdcllem3  16677  pcpre1  17026  pcqmul  17037  pcqcl  17040  prmgaplem3  17237  prmgaplem4  17238  xpsfrnel  17740  mreintcl  17771  isdrs  18481  isipodrs  18717  sgrp2rid2ex  19132  frgpuptinv  19991  isnzr2  20774  nrhmzr  20795  isdrng5  21014  isdrngrd  21029  isdrngrdOLD  21031  isprmidl  21625  psgnodpmr  21902  lindfrn  22133  dmatelnd  22817  dmatmul  22818  mdetdiaglem  22919  mdetunilem1  22933  fvmptnn04ifa  23174  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  fiinopn  23225  hausnei  23652  dfconn2  23743  2ndcdisj  23781  regr1lem2  24065  isfbas  24154  ioorinv  25903  ioorcl  25904  vitalilem2  25936  vitalilem3  25937  vitali  25940  itg1climres  26041  mbfi1fseqlem4  26045  dvferm1lem  26310  dvferm2lem  26312  isuc1p  26465  ismon1p  26467  ply1remlem  26489  plydivlem4  26623  aannenlem1  26661  aannenlem2  26662  lgsne0  27668  lgsqr  27684  nolesgn2ores  28035  nogesgn1ores  28037  nosepdmlem  28046  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noinfbnd2lem1  28093  axtg5seg  28933  axtgupdim2  28939  axtgeucl  28940  elcgrabasi  29381  axlowdim1  29543  lpvtx  29652  umgrnloopv  29690  usgrnloopvALT  29788  umgrvad2edg  29800  cusgrfilem2  30043  pthdlem2lem  30359  iswwlks  30431  iswwlksnx  30435  2pthdlem1  30525  isclwwlk  30581  3pthdlem1  30771  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eupth2lem2  30826  eupth2lem3lem4  30838  eupth2lem3lem6  30840  3cyclfrgrrn1  30892  4cycl2vnunb  30897  frgrreg  31001  norm1exi  31858  shintcl  31938  chintcl  31940  chne0  32102  elspansn2  32175  eigre  32443  eigorth  32446  kbpj  32564  superpos  32962  hatomic  32968  ismxidl  34034  ssmxidllem  34045  ssmxidl  34046  constrconj  34424  constrcccllem  34433  constrcbvlem  34434  2sqr3minply  34459  zarcmplem  34560  xrge0iifhom  34616  xrge0iif1  34617  esumpr2  34746  sibfof  35019  signswn0  35236  signswch  35237  signstfvneq0  35248  axtgupdim2ALTV  35344  bnj168  35408  bnj970  35624  bnj1154  35676  onvf1odlem2  35952  umgracycusgr  35996  cusgracyclt3v  35998  subfacp1lem1  36031  erdszelem8  36050  indispconn  36086  cvmsss2  36126  nepss  36576  elwlim  36678  dfrdg4  36808  fvray  36999  linedegen  37001  fvline  37002  hilbert1.1  37012  rankeq1o  37025  unblimceq0lem  37465  knoppndvlem21  37491  qdiff  38342  poimirlem1  38633  poimirlem17  38649  poimirlem20  38652  poimirlem32  38664  itg2addnclem3  38685  neificl  38781  isdrngo3  38987  ispridl  39062  ismaxidl  39068  islshp  40130  lsatn0  40150  lshpset2N  40270  atlex  40467  hlsuprexch  40532  3dimlem1  40609  llni2  40663  lplni2  40688  2llnjN  40718  lvoli2  40732  2lplnj  40771  islinei  40891  lnatexN  40930  llnexchb2  41020  lhpmatb  41182  cdleme40m  41618  cdlemftr3  41716  cdlemk28-3  42059  cdlemk35s  42088  cdlemk39s  42090  cdlemk42  42092  nnn1suc  43425  dnnumch1  44145  aomclem3  44152  aomclem8  44157  dfac11  44158  dfacbasgrp  44204  dfsucon  44618  ax6e2ndeq  45636  ax6e2ndeqVD  45985  relpfrlem  46037  permac8prim  46098  fnchoice  46140  fiiuncl  46176  disjrnmpt2  46297  idlimc  46732  limcperiod  46734  limclner  46755  cnrefiisp  46934  climxlim2lem  46949  fperdvper  47023  stoweidlem35  47139  stoweidlem43  47147  stoweidlem59  47163  fourierdlem76  47286  etransclem47  47385  nnfoctbdjlem  47559  elprneb  48193  ichexmpl1  48645  ichnreuop  48648  vopnbgrel  49046  dfclnbgr6  49048  dfnbgr6  49049  usgrgrtrirex  49142  isubgr3stgrlem4  49161  usgrexmpl2trifr  49229  gpg3kgrtriex  49281  itcoval2  49870  itcoval3  49871  itcovalsuc  49873  ackvalsuc1mpt  49884  inlinecirc02plem  49992  oppcthinendcALT  50670  fuconuniq2  50879  veronesev1lem  51142  veronesev2lem  51143  veronesev3lem  51144  veronesev4lem  51145  veronesev5lem  51146  veronesev6lem  51147  veronesevrowd  51148