Theorem neeq1 3000

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq1d 2997	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  pm13.18  3019  pm13.181  3020  nelrdva  3713  psseq1  4099  n0snor2el  4837  0inp0  5364  nnullss  5472  opeqex  5507  friOLD  5646  frsn  5775  xp11  6196  limeq  6397  tz6.12i  6934  fveqressseq  7098  funopsn  7167  fprg  7174  tpres  7220  f1dom3el3dif  7288  f1ounsn  7291  f1prex  7303  isofrlem  7359  f1oweALT  7995  frxp  8149  xpord2lem  8165  poxp2  8166  frxp2  8167  xpord2indlem  8170  xpord3lem  8172  frxp3  8174  xpord3inddlem  8177  suppimacnv  8197  elqsn0  8824  frfi  9318  fiint  9363  fiintOLD  9364  marypha1lem  9470  frmin  9786  eldju2ndl  9961  dfac8alem  10066  dfac8clem  10069  aceq3lem  10157  dfac5lem3  10162  dfac5lem4  10163  dfac5lem4OLD  10165  dfac5  10166  dfac2b  10168  dfac9  10174  kmlem1  10188  kmlem12  10199  kmlem14  10201  fin2i  10332  isfin2-2  10356  fin23lem21  10376  fin1a2lem10  10446  axcc2lem  10473  dominf  10482  ac5b  10515  zornn0g  10542  axdclem  10556  dominfac  10610  elwina  10723  elina  10724  iswun  10741  rankcf  10814  axrrecex  11200  elimne0  11248  1re  11258  recex  11892  xnn0nemnf  12607  uzn0  12892  qreccl  13008  xrnemnf  13156  xrnepnf  13157  xnn0n0n1ge2b  13170  fztpval  13622  expcl2lem  14110  hashnemnf  14379  hashneq0  14399  hashge2el2difr  14516  hashdmpropge2  14518  relexp1g  15061  ntrivcvgn0  15930  ntrivcvgmullem  15933  fprodntriv  15974  divalglem7  16432  divalg  16436  gcdcllem1  16532  gcdcllem3  16534  pcpre1  16875  pcqmul  16886  pcqcl  16889  prmgaplem3  17086  prmgaplem4  17087  xpsfrnel  17608  mreintcl  17639  isdrs  18358  isipodrs  18594  sgrp2rid2ex  18952  frgpuptinv  19803  isnzr2  20534  nrhmzr  20553  isdrngrd  20782  isdrngrdOLD  20784  psgnodpmr  21625  lindfrn  21858  dmatelnd  22517  dmatmul  22518  mdetdiaglem  22619  mdetunilem1  22633  fvmptnn04ifa  22871  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  fiinopn  22922  hausnei  23351  dfconn2  23442  2ndcdisj  23479  regr1lem2  23763  isfbas  23852  ioorinv  25624  ioorcl  25625  vitalilem2  25657  vitalilem3  25658  vitali  25661  itg1climres  25763  mbfi1fseqlem4  25767  dvferm1lem  26036  dvferm2lem  26038  isuc1p  26194  ismon1p  26196  ply1remlem  26218  plydivlem4  26352  aannenlem1  26384  aannenlem2  26385  lgsne0  27393  lgsqr  27409  nolesgn2ores  27731  nogesgn1ores  27733  nosepdmlem  27742  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  axtg5seg  28487  axtgupdim2  28493  axtgeucl  28494  axlowdim1  28988  lpvtx  29099  umgrnloopv  29137  usgrnloopvALT  29232  umgrvad2edg  29244  cusgrfilem2  29488  pthdlem2lem  29799  iswwlks  29865  iswwlksnx  29869  2pthdlem1  29959  isclwwlk  30012  3pthdlem1  30192  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2lem2  30247  eupth2lem3lem4  30259  eupth2lem3lem6  30261  3cyclfrgrrn1  30313  4cycl2vnunb  30318  frgrreg  30422  norm1exi  31278  shintcl  31358  chintcl  31360  chne0  31522  elspansn2  31595  eigre  31863  eigorth  31866  kbpj  31984  superpos  32382  hatomic  32388  isprmidl  33445  ismxidl  33469  ssmxidllem  33480  ssmxidl  33481  constrconj  33749  2sqr3minply  33752  zarcmplem  33841  xrge0iifhom  33897  xrge0iif1  33898  esumpr2  34047  sibfof  34321  signswn0  34553  signswch  34554  signstfvneq0  34565  axtgupdim2ALTV  34661  bnj168  34722  bnj970  34939  bnj1154  34991  umgracycusgr  35138  cusgracyclt3v  35140  subfacp1lem1  35163  erdszelem8  35182  indispconn  35218  cvmsss2  35258  nepss  35697  elwlim  35804  dfrdg4  35932  fvray  36122  linedegen  36124  fvline  36125  hilbert1.1  36135  rankeq1o  36152  unblimceq0lem  36488  knoppndvlem21  36514  poimirlem1  37607  poimirlem17  37623  poimirlem20  37626  poimirlem32  37638  itg2addnclem3  37659  neificl  37739  isdrngo3  37945  ispridl  38020  ismaxidl  38026  islshp  38960  lsatn0  38980  lshpset2N  39100  atlex  39297  hlsuprexch  39363  3dimlem1  39440  llni2  39494  lplni2  39519  2llnjN  39549  lvoli2  39563  2lplnj  39602  islinei  39722  lnatexN  39761  llnexchb2  39851  lhpmatb  40013  cdleme40m  40449  cdlemftr3  40547  cdlemk28-3  40890  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  metakunt30  42215  nnn1suc  42279  dnnumch1  43032  aomclem3  43044  aomclem8  43049  dfac11  43050  dfacbasgrp  43096  dfsucon  43512  ax6e2ndeq  44556  ax6e2ndeqVD  44906  fnchoice  44966  fiiuncl  45004  disjrnmpt2  45130  idlimc  45581  limcperiod  45583  limclner  45606  cnrefiisp  45785  climxlim2lem  45800  fperdvper  45874  stoweidlem35  45990  stoweidlem43  45998  stoweidlem59  46014  fourierdlem76  46137  etransclem47  46236  nnfoctbdjlem  46410  elprneb  46978  ichexmpl1  47393  ichnreuop  47396  vopnbgrel  47777  dfclnbgr6  47779  dfnbgr6  47780  usgrgrtrirex  47852  isubgr3stgrlem4  47871  usgrexmpl2trifr  47931  itcoval2  48513  itcoval3  48514  itcovalsuc  48516  ackvalsuc1mpt  48527  inlinecirc02plem  48635