Theorem neeq1 2712

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 23	. 2 |- ( A = B -> A = B )
2	1	neeq1d 2708	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   =/= wne 2625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-ne 2627

This theorem is referenced by:  neeq1iOLD  2717  neeq1dOLD  2722  nelrdva  3287  psseq1  3558  0inp0  4597  nnullss  4684  opeqex  4712  fri  4816  xp11  5292  limeq  5454  tz6.12i  5901  fveqressseq  6033  fprg  6088  tpres  6132  f1dom3el3dif  6184  f1prex  6197  isofrlem  6246  f1oweALT  6791  frxp  6917  suppimacnv  6936  elqsn0  7440  frfi  7822  fiint  7854  marypha1lem  7953  dfac8alem  8458  dfac8clem  8461  aceq3lem  8549  dfac5lem3  8554  dfac5lem4  8555  dfac5  8557  dfac2  8559  dfac9  8564  kmlem1  8578  kmlem12  8589  kmlem14  8591  fin2i  8723  isfin2-2  8747  fin23lem21  8767  fin1a2lem10  8837  axcc2lem  8864  dominf  8873  ac5b  8906  zornn0g  8933  axdclem  8947  dominfac  8996  elwina  9110  elina  9111  iswun  9128  rankcf  9201  axrrecex  9586  elimne0  9632  1re  9641  recex  10243  uzn0  11174  qreccl  11284  xrnemnf  11419  xrnepnf  11420  fztpval  11855  expcl2lem  12281  hashnemnf  12524  hashneq0  12542  relexp1g  13068  ntrivcvgn0  13932  ntrivcvgmullem  13935  fprodntriv  13974  divalglem7  14355  divalg  14359  gcdcllem1  14447  gcdcllem3  14449  isprm2lem  14602  pcpre1  14755  pcqmul  14766  pcqcl  14769  prmgaplem3  14986  prmgaplem4  14987  xpscfv  15419  xpsfrnel  15420  mreintcl  15452  isdrs  16130  isipodrs  16358  sgrp2rid2ex  16612  frgpuptinv  17356  isdrngrd  17936  isnzr2  18422  psgnodpmr  19089  lindfrn  19310  dmatelnd  19452  dmatmul  19453  mdetdiaglem  19554  mdetunilem1  19568  fvmptnn04ifa  19805  chfacfscmulgsum  19815  chfacfpmmulgsum  19819  fiinopn  19862  hausnei  20275  dfcon2  20365  2ndcdisj  20402  regr1lem2  20686  isfbas  20775  ioorinv  22405  ioorcl  22406  ioorinvOLD  22410  ioorclOLD  22411  vitalilem2  22444  vitalilem3  22445  vitali  22448  itg1climres  22549  mbfi1fseqlem4  22553  dvferm1lem  22813  dvferm2lem  22815  isuc1p  22966  ismon1p  22968  ply1remlem  22988  plydivlem4  23117  aannenlem1  23149  aannenlem2  23150  lgsne0  24124  lgsqr  24137  axtg5seg  24376  axtgupdim2  24382  axtgeucl  24383  axlowdim1  24835  usgranloopv  24951  usgra1v  24963  cusgrafilem2  25053  wlkn0  25100  2pthoncl  25178  iswwlk  25256  eupath2lem2  25551  eupath2lem3  25552  3cyclfrgrarn1  25585  4cycl2vnunb  25590  frgrawopreglem3  25619  norm1exi  26738  shintcl  26818  chintcl  26820  chne0  26982  elspansn2  27055  eigre  27323  eigorth  27326  kbpj  27444  superpos  27842  hatomic  27848  xrge0iifhom  28582  xrge0iif1  28583  esumpr2  28727  sibfof  29001  signswn0  29237  signswch  29238  signstfvneq0  29249  axtgupdim2OLD  29273  bnj168  29326  bnj970  29546  bnj1154  29596  subfacp1lem1  29690  erdszelem8  29709  indispcon  29745  cvmsss2  29785  nepss  30138  frmin  30267  elwlim  30293  dfrdg4  30503  fvray  30693  linedegen  30695  fvline  30696  hilbert1.1  30706  rankeq1o  30723  poimirlem1  31644  poimirlem17  31660  poimirlem20  31663  poimirlem32  31675  itg2addnclem3  31698  neificl  31785  isdrngo3  31901  ispridl  31970  ismaxidl  31976  islshp  32253  lsatn0  32273  lshpset2N  32393  atlex  32590  hlsuprexch  32654  3dimlem1  32731  llni2  32785  lplni2  32810  2llnjN  32840  lvoli2  32854  2lplnj  32893  islinei  33013  lnatexN  33052  llnexchb2  33142  lhpmatb  33304  cdleme40m  33742  cdlemftr3  33840  cdlemk28-3  34183  cdlemk35s  34212  cdlemk39s  34214  cdlemk42  34216  dnnumch1  35607  aomclem3  35619  aomclem8  35624  dfac11  35625  dfacbasgrp  35672  ax6e2ndeq  36562  ax6e2ndeqVD  36945  fnchoice  36989  fiiuncl  37047  disjrnmpt2  37085  idlimc  37277  limcperiod  37279  limclner  37303  fperdvper  37361  stoweidlem35  37464  stoweidlem43  37472  stoweidlem59  37488  fourierdlem76  37613  etransclem47  37712  nnfoctbdjlem  37801  elprneb  38101  usgvad2edg  38480  nrhmzr  38630