Theorem neeq1 3023

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  pm13.18  3042  pm13.181  3043  nelrdva  3671  psseq1  4047  n0snor2el  4803  0inp0  5334  nnullss  5448  opeqex  5486  frsn  5754  xp11  6178  limeq  6379  tz6.12i  6914  fveqressseq  7081  funopsnOLD  7152  fprg  7159  tpres  7206  f1dom3el3dif  7274  f1ounsn  7281  f1prex  7293  isofrlem  7349  resf1extb  7940  f1oweALT  7978  frxp  8131  xpord2lem  8147  poxp2  8148  frxp2  8149  xpord2indlem  8152  xpord3lem  8154  frxp3  8156  xpord3inddlem  8159  suppimacnv  8179  elqsn0  8791  frfi  9255  fiint  9296  marypha1lem  9403  frmin  9731  eldju2ndl  9929  dfac8alem  10032  dfac8clem  10035  aceq3lem  10123  dfac5lem3  10128  dfac5lem4  10129  dfac5  10131  dfac2b  10133  dfac9  10139  kmlem1  10153  kmlem12  10164  kmlem14  10166  fin2i  10297  isfin2-2  10321  fin23lem21  10341  fin1a2lem10  10411  axcc2lem  10438  dominf  10447  ac5b  10480  zornn0g  10507  axdclem  10521  dominfac  10576  elwina  10689  elina  10690  iswun  10707  rankcf  10780  axrrecex  11166  elimne0  11214  1re  11226  recex  11864  xnn0nemnf  12606  uzn0  12897  qreccl  13011  xrnemnf  13160  xrnepnf  13161  xnn0n0n1ge2b  13175  fztpval  13633  expcl2lem  14129  hashnemnf  14400  hashneq0  14420  hashge2el2difr  14538  hashdmpropge2  14540  relexp1g  15089  ntrivcvgn0  15978  ntrivcvgmullem  15981  fprodntriv  16022  divalglem7  16482  divalg  16486  gcdcllem1  16582  gcdcllem3  16584  pcpre1  16927  pcqmul  16938  pcqcl  16941  prmgaplem3  17138  prmgaplem4  17139  xpsfrnel  17641  mreintcl  17672  isdrs  18382  isipodrs  18618  sgrp2rid2ex  19020  frgpuptinv  19872  isnzr2  20652  nrhmzr  20673  isdrng5  20891  isdrngrd  20906  isdrngrdOLD  20908  isprmidl  21500  psgnodpmr  21777  lindfrn  22008  dmatelnd  22690  dmatmul  22691  mdetdiaglem  22792  mdetunilem1  22806  fvmptnn04ifa  23044  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  fiinopn  23095  hausnei  23522  dfconn2  23613  2ndcdisj  23650  regr1lem2  23934  isfbas  24023  ioorinv  25772  ioorcl  25773  vitalilem2  25805  vitalilem3  25806  vitali  25809  itg1climres  25910  mbfi1fseqlem4  25914  dvferm1lem  26180  dvferm2lem  26182  isuc1p  26335  ismon1p  26337  ply1remlem  26359  plydivlem4  26494  aannenlem1  26528  aannenlem2  26529  lgsne0  27536  lgsqr  27552  nolesgn2ores  27873  nogesgn1ores  27875  nosepdmlem  27884  nosupbnd1lem3  27911  nosupbnd1lem5  27913  nosupbnd2lem1  27916  noinfbnd1lem3  27926  noinfbnd1lem5  27928  noinfbnd2lem1  27931  axtg5seg  28771  axtgupdim2  28777  axtgeucl  28778  axlowdim1  29346  lpvtx  29455  umgrnloopv  29493  usgrnloopvALT  29588  umgrvad2edg  29600  cusgrfilem2  29843  pthdlem2lem  30153  iswwlks  30222  iswwlksnx  30226  2pthdlem1  30316  isclwwlk  30372  3pthdlem1  30552  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eupth2lem2  30607  eupth2lem3lem4  30619  eupth2lem3lem6  30621  3cyclfrgrrn1  30673  4cycl2vnunb  30678  frgrreg  30782  norm1exi  31639  shintcl  31719  chintcl  31721  chne0  31883  elspansn2  31956  eigre  32224  eigorth  32227  kbpj  32345  superpos  32743  hatomic  32749  ismxidl  33776  ssmxidllem  33787  ssmxidl  33788  constrconj  34166  constrcccllem  34175  constrcbvlem  34176  2sqr3minply  34201  zarcmplem  34302  xrge0iifhom  34358  xrge0iif1  34359  esumpr2  34488  sibfof  34762  signswn0  34979  signswch  34980  signstfvneq0  34991  axtgupdim2ALTV  35087  bnj168  35151  bnj970  35367  bnj1154  35419  onvf1odlem2  35612  umgracycusgr  35667  cusgracyclt3v  35669  subfacp1lem1  35692  erdszelem8  35711  indispconn  35747  cvmsss2  35787  nepss  36231  elwlim  36334  dfrdg4  36464  fvray  36654  linedegen  36656  fvline  36657  hilbert1.1  36667  rankeq1o  36684  unblimceq0lem  37136  knoppndvlem21  37162  qdiff  38012  poimirlem1  38313  poimirlem17  38329  poimirlem20  38332  poimirlem32  38344  itg2addnclem3  38365  neificl  38445  isdrngo3  38651  ispridl  38726  ismaxidl  38732  islshp  39794  lsatn0  39814  lshpset2N  39934  atlex  40131  hlsuprexch  40196  3dimlem1  40273  llni2  40327  lplni2  40352  2llnjN  40382  lvoli2  40396  2lplnj  40435  islinei  40555  lnatexN  40594  llnexchb2  40684  lhpmatb  40846  cdleme40m  41282  cdlemftr3  41380  cdlemk28-3  41723  cdlemk35s  41752  cdlemk39s  41754  cdlemk42  41756  nnn1suc  43074  dnnumch1  43812  aomclem3  43824  aomclem8  43829  dfac11  43830  dfacbasgrp  43876  dfsucon  44290  ax6e2ndeq  45309  ax6e2ndeqVD  45658  relpfrlem  45703  permac8prim  45764  fnchoice  45790  fiiuncl  45826  disjrnmpt2  45947  idlimc  46383  limcperiod  46385  limclner  46406  cnrefiisp  46585  climxlim2lem  46600  fperdvper  46674  stoweidlem35  46790  stoweidlem43  46798  stoweidlem59  46814  fourierdlem76  46937  etransclem47  47036  nnfoctbdjlem  47210  elprneb  47807  ichexmpl1  48259  ichnreuop  48262  vopnbgrel  48660  dfclnbgr6  48662  dfnbgr6  48663  usgrgrtrirex  48756  isubgr3stgrlem4  48775  usgrexmpl2trifr  48843  gpg3kgrtriex  48895  itcoval2  49485  itcoval3  49486  itcovalsuc  49488  ackvalsuc1mpt  49499  inlinecirc02plem  49607  oppcthinendcALT  50260