Theorem neeq1 3019

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

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

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 2734

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

This theorem is used by:  pm13.18  3038  pm13.181  3039  nelrdva  3666  psseq1  4041  n0snor2el  4796  0inp0  5327  nnullss  5441  opeqex  5479  frsn  5747  xp11  6172  limeq  6373  tz6.12i  6908  fveqressseq  7076  funopsnOLD  7149  fprg  7156  tpres  7204  f1dom3el3dif  7270  f1ounsn  7277  f1prex  7289  isofrlem  7345  resf1extb  7935  f1oweALT  7973  frxp  8128  xpord2lem  8144  poxp2  8145  frxp2  8146  xpord2indlem  8149  xpord3lem  8151  frxp3  8153  xpord3inddlem  8156  suppimacnv  8176  elqsn0  8788  frfi  9259  fiint  9300  marypha1lem  9407  frmin  9735  eldju2ndl  9933  dfac8alem  10036  dfac8clem  10039  aceq3lem  10127  dfac5lem3  10132  dfac5lem4  10133  dfac5  10135  dfac2b  10137  dfac9  10143  kmlem1  10157  kmlem12  10168  kmlem14  10170  fin2i  10301  isfin2-2  10325  fin23lem21  10345  fin1a2lem10  10415  axcc2lem  10442  dominf  10451  ac5b  10484  zornn0g  10511  axdclem  10525  dominfac  10586  elwina  10699  elina  10700  iswun  10717  rankcf  10790  axrrecex  11176  elimne0  11224  1re  11236  recex  11874  xnn0nemnf  12616  uzn0  12908  qreccl  13023  xrnemnf  13172  xrnepnf  13173  xnn0n0n1ge2b  13187  fztpval  13645  expcl2lem  14141  hashnemnf  14412  hashneq0  14432  hashge2el2difr  14550  hashdmpropge2  14552  relexp1g  15103  ntrivcvgn0  15991  ntrivcvgmullem  15994  fprodntriv  16035  divalglem7  16495  divalg  16499  gcdcllem1  16595  gcdcllem3  16597  pcpre1  16940  pcqmul  16951  pcqcl  16954  prmgaplem3  17151  prmgaplem4  17152  xpsfrnel  17654  mreintcl  17685  isdrs  18395  isipodrs  18631  sgrp2rid2ex  19045  frgpuptinv  19904  isnzr2  20684  nrhmzr  20705  isdrng5  20923  isdrngrd  20938  isdrngrdOLD  20940  isprmidl  21532  psgnodpmr  21809  lindfrn  22040  dmatelnd  22724  dmatmul  22725  mdetdiaglem  22826  mdetunilem1  22840  fvmptnn04ifa  23081  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  fiinopn  23132  hausnei  23559  dfconn2  23650  2ndcdisj  23688  regr1lem2  23972  isfbas  24061  ioorinv  25810  ioorcl  25811  vitalilem2  25843  vitalilem3  25844  vitali  25847  itg1climres  25948  mbfi1fseqlem4  25952  dvferm1lem  26218  dvferm2lem  26220  isuc1p  26373  ismon1p  26375  ply1remlem  26397  plydivlem4  26533  aannenlem1  26571  aannenlem2  26572  lgsne0  27579  lgsqr  27595  nolesgn2ores  27916  nogesgn1ores  27918  nosepdmlem  27927  nosupbnd1lem3  27954  nosupbnd1lem5  27956  nosupbnd2lem1  27959  noinfbnd1lem3  27969  noinfbnd1lem5  27971  noinfbnd2lem1  27974  axtg5seg  28814  axtgupdim2  28820  axtgeucl  28821  elcgrabasi  29262  axlowdim1  29424  lpvtx  29533  umgrnloopv  29571  usgrnloopvALT  29669  umgrvad2edg  29681  cusgrfilem2  29924  pthdlem2lem  30240  iswwlks  30312  iswwlksnx  30316  2pthdlem1  30406  isclwwlk  30462  3pthdlem1  30652  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eupth2lem2  30707  eupth2lem3lem4  30719  eupth2lem3lem6  30721  3cyclfrgrrn1  30773  4cycl2vnunb  30778  frgrreg  30882  norm1exi  31739  shintcl  31819  chintcl  31821  chne0  31983  elspansn2  32056  eigre  32324  eigorth  32327  kbpj  32445  superpos  32843  hatomic  32849  ismxidl  33873  ssmxidllem  33884  ssmxidl  33885  constrconj  34263  constrcccllem  34272  constrcbvlem  34273  2sqr3minply  34298  zarcmplem  34399  xrge0iifhom  34455  xrge0iif1  34456  esumpr2  34585  sibfof  34859  signswn0  35076  signswch  35077  signstfvneq0  35088  axtgupdim2ALTV  35184  bnj168  35248  bnj970  35464  bnj1154  35516  onvf1odlem2  35709  umgracycusgr  35741  cusgracyclt3v  35743  subfacp1lem1  35766  erdszelem8  35785  indispconn  35821  cvmsss2  35861  nepss  36305  elwlim  36408  dfrdg4  36538  fvray  36729  linedegen  36731  fvline  36732  hilbert1.1  36742  rankeq1o  36759  unblimceq0lem  37211  knoppndvlem21  37237  qdiff  38087  poimirlem1  38378  poimirlem17  38394  poimirlem20  38397  poimirlem32  38409  itg2addnclem3  38430  neificl  38511  isdrngo3  38717  ispridl  38792  ismaxidl  38798  islshp  39860  lsatn0  39880  lshpset2N  40000  atlex  40197  hlsuprexch  40262  3dimlem1  40339  llni2  40393  lplni2  40418  2llnjN  40448  lvoli2  40462  2lplnj  40501  islinei  40621  lnatexN  40660  llnexchb2  40750  lhpmatb  40912  cdleme40m  41348  cdlemftr3  41446  cdlemk28-3  41789  cdlemk35s  41818  cdlemk39s  41820  cdlemk42  41822  nnn1suc  43155  dnnumch1  43893  aomclem3  43905  aomclem8  43910  dfac11  43911  dfacbasgrp  43957  dfsucon  44371  ax6e2ndeq  45390  ax6e2ndeqVD  45739  relpfrlem  45784  permac8prim  45845  fnchoice  45871  fiiuncl  45907  disjrnmpt2  46028  idlimc  46464  limcperiod  46466  limclner  46487  cnrefiisp  46666  climxlim2lem  46681  fperdvper  46755  stoweidlem35  46871  stoweidlem43  46879  stoweidlem59  46895  fourierdlem76  47018  etransclem47  47117  nnfoctbdjlem  47291  elprneb  47925  ichexmpl1  48377  ichnreuop  48380  vopnbgrel  48778  dfclnbgr6  48780  dfnbgr6  48781  usgrgrtrirex  48874  isubgr3stgrlem4  48893  usgrexmpl2trifr  48961  gpg3kgrtriex  49013  itcoval2  49602  itcoval3  49603  itcovalsuc  49605  ackvalsuc1mpt  49616  inlinecirc02plem  49724  oppcthinendcALT  50375  veronesev1lem  50814  veronesev2lem  50815  veronesev3lem  50816  veronesev4lem  50817  veronesev5lem  50818  veronesev6lem  50819  veronesevrowd  50820