Theorem neeq1 2748

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 2744	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  neeq1iOLD  2753  neeq1dOLD  2758  nelrdva  3313  psseq1  3591  0inp0  4619  nnullss  4709  opeqex  4738  fri  4841  limeq  4890  xp11  5440  tz6.12i  5884  fprg  6068  f1dom3el3dif  6162  isofrlem  6222  f1oweALT  6765  frxp  6890  suppimacnv  6909  elqsn0  7377  frfi  7761  fiint  7793  marypha1lem  7889  dfac8alem  8406  dfac8clem  8409  aceq3lem  8497  dfac5lem3  8502  dfac5lem4  8503  dfac5  8505  dfac2  8507  dfac9  8512  kmlem1  8526  kmlem12  8537  kmlem14  8539  fin2i  8671  isfin2-2  8695  fin23lem21  8715  fin1a2lem10  8785  axcc2lem  8812  dominf  8821  ac5b  8854  zornn0g  8881  axdclem  8895  dominfac  8944  elwina  9060  elina  9061  iswun  9078  rankcf  9151  axrrecex  9536  elimne0  9582  1re  9591  recex  10177  uzn0  11093  qreccl  11198  xrnemnf  11324  xrnepnf  11325  fztpval  11737  expcl2lem  12142  hashnemnf  12381  hashneq0  12398  divalglem7  13912  divalg  13916  gcdcllem1  14004  gcdcllem3  14006  isprm2lem  14079  pcpre1  14221  pcqmul  14232  pcqcl  14235  xpscfv  14813  xpsfrnel  14814  mreintcl  14846  isdrs  15417  isipodrs  15644  frgpuptinv  16585  isdrngrd  17205  isnzr2  17693  psgnodpmr  18393  lindfrn  18623  dmatelnd  18765  dmatmul  18766  mdetdiaglem  18867  mdetunilem1  18881  fvmptnn04ifa  19118  chfacfscmulgsum  19128  chfacfpmmulgsum  19132  fiinopn  19177  hausnei  19595  dfcon2  19686  2ndcdisj  19723  regr1lem2  19976  isfbas  20065  ioorinv  21720  ioorcl  21721  vitalilem2  21753  vitalilem3  21754  vitali  21757  itg1climres  21856  mbfi1fseqlem4  21860  dvferm1lem  22120  dvferm2lem  22122  isuc1p  22276  ismon1p  22278  ply1remlem  22298  plydivlem4  22426  aannenlem1  22458  aannenlem2  22459  lgsne0  23336  lgsqr  23349  axtg5seg  23590  axtgupdim2  23597  axtgeucl  23598  axlowdim1  23938  usgranloopv  24054  usgra1v  24066  cusgrafilem2  24156  wlkn0  24203  2pthoncl  24281  iswwlk  24359  eupath2lem2  24654  eupath2lem3  24655  3cyclfrgrarn1  24688  4cycl2vnunb  24693  frgrawopreglem3  24723  norm1exi  25844  shintcl  25924  chintcl  25926  chne0  26088  elspansn2  26161  eigre  26430  eigorth  26433  kbpj  26551  superpos  26949  hatomic  26955  xrge0iifhom  27555  xrge0iif1  27556  esumpr2  27714  sibfof  27922  signswn0  28157  signswch  28158  signstfvneq0  28169  subfacp1lem1  28263  erdszelem8  28282  indispcon  28319  cvmsss2  28359  nepss  28570  ntrivcvgn0  28609  ntrivcvgmullem  28612  fprodntriv  28651  frmin  28899  elwlim  28956  dfrdg4  29177  fvray  29368  linedegen  29370  fvline  29371  hilbert1.1  29381  rankeq1o  29405  itg2addnclem3  29645  neificl  29849  isdrngo3  29965  ispridl  30034  ismaxidl  30040  dnnumch1  30594  aomclem3  30606  aomclem8  30611  dfac11  30612  dfacbasgrp  30661  fnchoice  30982  idlimc  31168  limcperiod  31170  limclner  31193  fperdvper  31248  stoweidlem35  31335  stoweidlem43  31343  stoweidlem59  31359  fourierdlem76  31483  usgvad2edg  31880  ax6e2ndeq  32412  ax6e2ndeqVD  32789  bnj168  32865  bnj970  33084  bnj1154  33134  islshp  33776  lsatn0  33796  lshpset2N  33916  atlex  34113  hlsuprexch  34177  3dimlem1  34254  llni2  34308  lplni2  34333  2llnjN  34363  lvoli2  34377  2lplnj  34416  islinei  34536  lnatexN  34575  llnexchb2  34665  lhpmatb  34827  cdleme40m  35263  cdlemftr3  35361  cdlemk28-3  35704  cdlemk35s  35733  cdlemk39s  35735  cdlemk42  35737