Theorem neeq1 3021

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  pm13.18  3040  pm13.181  3041  nelrdva  3666  psseq1  4020  n0snor2el  4791  0inp0  5325  nnullss  5435  opeqex  5475  frsn  5745  xp11  6180  limeq  6395  tz6.12i  6937  fveqressseq  7106  funopsnOLD  7179  fprg  7186  tpres  7233  f1dom3el3dif  7299  f1ounsn  7306  f1prex  7318  isofrlem  7374  resf1extb  7973  f1oweALT  8011  frxp  8168  xpord2lem  8189  poxp2  8190  frxp2  8191  xpord2indlem  8194  xpord3lem  8196  frxp3  8198  xpord3inddlem  8201  suppimacnv  8222  elqsn0  8836  frfi  9307  fiint  9349  marypha1lem  9455  frmin  9783  eldju2ndl  10035  dfac8alem  10138  dfac8clem  10141  aceq3lem  10229  dfac5lem3  10234  dfac5lem4  10235  dfac5  10237  dfac2b  10239  dfac9  10245  kmlem1  10259  kmlem12  10270  kmlem14  10272  fin2i  10403  isfin2-2  10427  fin23lem21  10447  fin1a2lem10  10517  axcc2lem  10544  dominf  10553  ac5b  10586  zornn0g  10613  axdclem  10627  dominfac  10688  elwina  10801  elina  10802  iswun  10819  rankcf  10892  axrrecex  11278  elimne0  11326  1re  11338  recex  11978  xnn0nemnf  12720  uzn0  13012  qreccl  13127  xrnemnf  13276  xrnepnf  13277  xnn0n0n1ge2b  13291  fztpval  13750  expcl2lem  14246  hashnemnf  14518  hashneq0  14538  hashge2el2difr  14656  hashdmpropge2  14658  relexp1g  15211  ntrivcvgn0  16099  ntrivcvgmullem  16102  fprodntriv  16141  divalglem7  16601  divalg  16605  gcdcllem1  16701  gcdcllem3  16703  pcpre1  17052  pcqmul  17063  pcqcl  17066  prmgaplem3  17263  prmgaplem4  17264  xpsfrnel  17766  mreintcl  17797  isdrs  18507  isipodrs  18743  sgrp2rid2ex  19158  frgpuptinv  20018  isnzr2  20801  nrhmzr  20822  isdrng5  21041  isdrngrd  21056  isdrngrdOLD  21058  isprmidl  21652  psgnodpmr  21929  lindfrn  22160  dmatelnd  22844  dmatmul  22845  mdetdiaglem  22946  mdetunilem1  22960  fvmptnn04ifa  23201  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  fiinopn  23252  hausnei  23679  dfconn2  23770  2ndcdisj  23808  regr1lem2  24092  isfbas  24181  ioorinv  25930  ioorcl  25931  vitalilem2  25963  vitalilem3  25964  vitali  25967  itg1climres  26068  mbfi1fseqlem4  26072  dvferm1lem  26337  dvferm2lem  26339  isuc1p  26492  ismon1p  26494  ply1remlem  26516  plydivlem4  26650  aannenlem1  26688  aannenlem2  26689  lgsne0  27695  lgsqr  27711  nolesgn2ores  28062  nogesgn1ores  28064  nosepdmlem  28073  nosupbnd1lem3  28100  nosupbnd1lem5  28102  nosupbnd2lem1  28105  noinfbnd1lem3  28115  noinfbnd1lem5  28117  noinfbnd2lem1  28120  axtg5seg  28960  axtgupdim2  28966  axtgeucl  28967  elcgrabasi  29408  axlowdim1  29570  lpvtx  29679  umgrnloopv  29717  usgrnloopvALT  29815  umgrvad2edg  29827  cusgrfilem2  30070  pthdlem2lem  30386  iswwlks  30458  iswwlksnx  30462  2pthdlem1  30552  isclwwlk  30608  3pthdlem1  30798  upgr3v3e3cycl  30814  upgr4cycl4dv4e  30819  eupth2lem2  30853  eupth2lem3lem4  30865  eupth2lem3lem6  30867  3cyclfrgrrn1  30919  4cycl2vnunb  30924  frgrreg  31028  norm1exi  31885  shintcl  31965  chintcl  31967  chne0  32129  elspansn2  32202  eigre  32470  eigorth  32473  kbpj  32591  superpos  32989  hatomic  32995  ismxidl  34071  ssmxidllem  34082  ssmxidl  34083  constrconj  34460  constrcccllem  34469  constrcbvlem  34470  2sqr3minply  34495  zarcmplem  34596  xrge0iifhom  34652  xrge0iif1  34653  esumpr2  34782  sibfof  35055  signswn0  35272  signswch  35273  signstfvneq0  35284  axtgupdim2ALTV  35380  bnj168  35444  bnj970  35660  bnj1154  35712  onvf1odlem2  36045  umgracycusgr  36089  cusgracyclt3v  36091  subfacp1lem1  36124  erdszelem8  36143  indispconn  36179  cvmsss2  36219  nepss  36674  elwlim  36776  dfrdg4  36906  fvray  37097  linedegen  37099  fvline  37100  hilbert1.1  37110  rankeq1o  37123  unblimceq0lem  37563  knoppndvlem21  37589  qdiff  38453  poimirlem1  38744  poimirlem17  38760  poimirlem20  38763  poimirlem32  38775  itg2addnclem3  38796  neificl  38890  isdrngo3  39096  ispridl  39171  ismaxidl  39177  islshp  40239  lsatn0  40259  lshpset2N  40379  atlex  40576  hlsuprexch  40641  3dimlem1  40718  llni2  40772  lplni2  40797  2llnjN  40827  lvoli2  40841  2lplnj  40880  islinei  41000  lnatexN  41039  llnexchb2  41129  lhpmatb  41291  cdleme40m  41727  cdlemftr3  41825  cdlemk28-3  42168  cdlemk35s  42197  cdlemk39s  42199  cdlemk42  42201  nnn1suc  43535  dnnumch1  44255  aomclem3  44262  aomclem8  44267  dfac11  44268  dfacbasgrp  44313  dfsucon  44727  ax6e2ndeq  45744  ax6e2ndeqVD  46093  relpfrlem  46149  permac8prim  46210  fnchoice  46262  fiiuncl  46298  disjrnmpt2  46418  idlimc  46853  limcperiod  46855  limclner  46876  cnrefiisp  47055  climxlim2lem  47070  fperdvper  47144  stoweidlem35  47260  stoweidlem43  47268  stoweidlem59  47284  fourierdlem76  47407  etransclem47  47506  nnfoctbdjlem  47680  elprneb  48314  ichexmpl1  48766  ichnreuop  48769  vopnbgrel  49167  dfclnbgr6  49169  dfnbgr6  49170  usgrgrtrirex  49263  isubgr3stgrlem4  49282  usgrexmpl2trifr  49350  gpg3kgrtriex  49402  itcoval2  49991  itcoval3  49992  itcovalsuc  49994  ackvalsuc1mpt  50005  inlinecirc02plem  50113  oppcthinendcALT  50791  fuconuniq2  51000  veronesev1lem  51285  veronesev2lem  51286  veronesev3lem  51287  veronesev4lem  51288  veronesev5lem  51289  veronesev6lem  51290  veronesevrowd  51291