Theorem neeq1 2686

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq1	|- ( A = B -> ( A =/= C <-> B =/= C ) )

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( A = B -> A = B )
2	1	neeq1d 2683	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   =/= wne 2622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624

This theorem is referenced by:  nelrdva  3249  psseq1  3520  0inp0  4575  nnullss  4662  opeqex  4692  fri  4796  xp11  5272  limeq  5435  tz6.12i  5885  fveqressseq  6018  fprg  6073  tpres  6117  f1dom3el3dif  6169  f1prex  6182  isofrlem  6231  f1oweALT  6777  frxp  6906  suppimacnv  6925  elqsn0  7432  frfi  7816  fiint  7848  marypha1lem  7947  dfac8alem  8460  dfac8clem  8463  aceq3lem  8551  dfac5lem3  8556  dfac5lem4  8557  dfac5  8559  dfac2  8561  dfac9  8566  kmlem1  8580  kmlem12  8591  kmlem14  8593  fin2i  8725  isfin2-2  8749  fin23lem21  8769  fin1a2lem10  8839  axcc2lem  8866  dominf  8875  ac5b  8908  zornn0g  8935  axdclem  8949  dominfac  8998  elwina  9111  elina  9112  iswun  9129  rankcf  9202  axrrecex  9587  elimne0  9633  1re  9642  recex  10244  uzn0  11174  qreccl  11284  xrnemnf  11419  xrnepnf  11420  fztpval  11857  expcl2lem  12284  hashnemnf  12527  hashneq0  12545  hashge2el2difr  12638  relexp1g  13089  ntrivcvgn0  13954  ntrivcvgmullem  13957  fprodntriv  13996  divalglem7  14379  divalg  14384  gcdcllem1  14473  gcdcllem3  14475  isprm2lem  14631  pcpre1  14792  pcqmul  14803  pcqcl  14806  prmgaplem3  15023  prmgaplem4  15024  xpscfv  15468  xpsfrnel  15469  mreintcl  15501  isdrs  16179  isipodrs  16407  sgrp2rid2ex  16661  frgpuptinv  17421  isdrngrd  18001  isnzr2  18487  psgnodpmr  19158  lindfrn  19379  dmatelnd  19521  dmatmul  19522  mdetdiaglem  19623  mdetunilem1  19637  fvmptnn04ifa  19874  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  fiinopn  19931  hausnei  20344  dfcon2  20434  2ndcdisj  20471  regr1lem2  20755  isfbas  20844  ioorinv  22528  ioorcl  22529  ioorinvOLD  22533  ioorclOLD  22534  vitalilem2  22567  vitalilem3  22568  vitali  22571  itg1climres  22672  mbfi1fseqlem4  22676  dvferm1lem  22936  dvferm2lem  22938  isuc1p  23091  ismon1p  23093  ply1remlem  23113  plydivlem4  23249  aannenlem1  23284  aannenlem2  23285  lgsne0  24261  lgsqr  24274  axtg5seg  24513  axtgupdim2  24519  axtgeucl  24520  axlowdim1  24989  usgranloopv  25105  usgra1v  25117  cusgrafilem2  25208  wlkn0  25255  2pthoncl  25333  iswwlk  25411  eupath2lem2  25706  eupath2lem3  25707  3cyclfrgrarn1  25740  4cycl2vnunb  25745  frgrawopreglem3  25774  norm1exi  26903  shintcl  26983  chintcl  26985  chne0  27147  elspansn2  27220  eigre  27488  eigorth  27491  kbpj  27609  superpos  28007  hatomic  28013  xrge0iifhom  28743  xrge0iif1  28744  esumpr2  28888  sibfof  29173  signswn0  29449  signswch  29450  signstfvneq0  29461  axtgupdim2OLD  29485  bnj168  29538  bnj970  29758  bnj1154  29808  subfacp1lem1  29902  erdszelem8  29921  indispcon  29957  cvmsss2  29997  nepss  30350  frmin  30480  elwlim  30506  dfrdg4  30718  fvray  30908  linedegen  30910  fvline  30911  hilbert1.1  30921  rankeq1o  30938  poimirlem1  31941  poimirlem17  31957  poimirlem20  31960  poimirlem32  31972  itg2addnclem3  31995  neificl  32082  isdrngo3  32198  ispridl  32267  ismaxidl  32273  islshp  32545  lsatn0  32565  lshpset2N  32685  atlex  32882  hlsuprexch  32946  3dimlem1  33023  llni2  33077  lplni2  33102  2llnjN  33132  lvoli2  33146  2lplnj  33185  islinei  33305  lnatexN  33344  llnexchb2  33434  lhpmatb  33596  cdleme40m  34034  cdlemftr3  34132  cdlemk28-3  34475  cdlemk35s  34504  cdlemk39s  34506  cdlemk42  34508  dnnumch1  35902  aomclem3  35914  aomclem8  35919  dfac11  35920  dfacbasgrp  35967  ax6e2ndeq  36926  ax6e2ndeqVD  37306  fnchoice  37350  fiiuncl  37406  disjrnmpt2  37463  idlimc  37706  limcperiod  37708  limclner  37732  fperdvper  37790  stoweidlem35  37896  stoweidlem43  37904  stoweidlem59  37920  fourierdlem76  38046  etransclem47  38146  nnfoctbdjlem  38293  elprneb  38712  n0snor2el  38996  funopsn  39018  xnn0nemnf  39082  structgrssvtxlem  39125  umgrnloopv  39194  usgrnloopvALT  39284  usgr1vr  39329  cusgrfilem2  39517  1wlkn0  39636  1wlkvtxiedg  39638  usgvad2edg  39776  nrhmzr  39926