Theorem neeq1 2856

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  nelrdva  3417  psseq1  3694  ssdifsn  4318  n0snor2el  4364  0inp0  4837  nnullss  4930  opeqex  4962  fri  5076  frsn  5189  xp11  5569  limeq  5735  tz6.12i  6214  fveqressseq  6355  funopsn  6413  fprg  6422  tpres  6466  f1dom3el3dif  6526  f1prex  6539  isofrlem  6590  f1oweALT  7152  frxp  7287  suppimacnv  7306  elqsn0  7816  frfi  8205  fiint  8237  marypha1lem  8339  dfac8alem  8852  dfac8clem  8855  aceq3lem  8943  dfac5lem3  8948  dfac5lem4  8949  dfac5  8951  dfac2  8953  dfac9  8958  kmlem1  8972  kmlem12  8983  kmlem14  8985  fin2i  9117  isfin2-2  9141  fin23lem21  9161  fin1a2lem10  9231  axcc2lem  9258  dominf  9267  ac5b  9300  zornn0g  9327  axdclem  9341  dominfac  9395  elwina  9508  elina  9509  iswun  9526  rankcf  9599  axrrecex  9984  elimne0  10030  1re  10039  recex  10659  xnn0nemnf  11374  uzn0  11703  qreccl  11808  xrnemnf  11951  xrnepnf  11952  xnn0n0n1ge2b  11965  fztpval  12402  expcl2lem  12872  hashnemnf  13132  hashneq0  13155  hashge2el2difr  13263  hashdmpropge2  13265  relexp1g  13766  ntrivcvgn0  14630  ntrivcvgmullem  14633  fprodntriv  14672  divalglem7  15122  divalg  15126  gcdcllem1  15221  gcdcllem3  15223  pcpre1  15547  pcqmul  15558  pcqcl  15561  prmgaplem3  15757  prmgaplem4  15758  xpscfv  16222  xpsfrnel  16223  mreintcl  16255  isdrs  16934  isipodrs  17161  sgrp2rid2ex  17414  frgpuptinv  18184  isdrngrd  18773  isnzr2  19263  psgnodpmr  19936  lindfrn  20160  dmatelnd  20302  dmatmul  20303  mdetdiaglem  20404  mdetunilem1  20418  fvmptnn04ifa  20655  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  fiinopn  20706  hausnei  21132  dfconn2  21222  2ndcdisj  21259  regr1lem2  21543  isfbas  21633  ioorinv  23344  ioorcl  23345  vitalilem2  23378  vitalilem3  23379  vitali  23382  itg1climres  23481  mbfi1fseqlem4  23485  dvferm1lem  23747  dvferm2lem  23749  isuc1p  23900  ismon1p  23902  ply1remlem  23922  plydivlem4  24051  aannenlem1  24083  aannenlem2  24084  lgsne0  25060  lgsqr  25076  axtg5seg  25364  axtgupdim2  25370  axtgeucl  25371  axlowdim1  25839  structgrssvtxlemOLD  25915  lpvtx  25963  umgrnloopv  26001  usgrnloopvALT  26093  umgrvad2edg  26105  cusgrfilem2  26352  pthdlem2lem  26663  iswwlks  26728  iswwlksnx  26731  2pthdlem1  26826  isclwwlks  26880  3pthdlem1  27024  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth2lem2  27079  eupth2lem3lem4  27091  eupth2lem3lem6  27093  3cyclfrgrrn1  27149  4cycl2vnunb  27154  frgrreg  27252  norm1exi  28107  shintcl  28189  chintcl  28191  chne0  28353  elspansn2  28426  eigre  28694  eigorth  28697  kbpj  28815  superpos  29213  hatomic  29219  xrge0iifhom  29983  xrge0iif1  29984  esumpr2  30129  sibfof  30402  signswn0  30637  signswch  30638  signstfvneq0  30649  axtgupdim2OLD  30746  bnj168  30798  bnj970  31017  bnj1154  31067  subfacp1lem1  31161  erdszelem8  31180  indispconn  31216  cvmsss2  31256  nepss  31599  frmin  31739  elwlim  31769  elwlimOLD  31770  nolesgn2ores  31825  nosepdmlem  31833  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  dfrdg4  32058  fvray  32248  linedegen  32250  fvline  32251  hilbert1.1  32261  rankeq1o  32278  unblimceq0lem  32497  knoppndvlem21  32523  poimirlem1  33410  poimirlem17  33426  poimirlem20  33429  poimirlem32  33441  itg2addnclem3  33463  neificl  33549  isdrngo3  33758  ispridl  33833  ismaxidl  33839  islshp  34266  lsatn0  34286  lshpset2N  34406  atlex  34603  hlsuprexch  34667  3dimlem1  34744  llni2  34798  lplni2  34823  2llnjN  34853  lvoli2  34867  2lplnj  34906  islinei  35026  lnatexN  35065  llnexchb2  35155  lhpmatb  35317  cdleme40m  35755  cdlemftr3  35853  cdlemk28-3  36196  cdlemk35s  36225  cdlemk39s  36227  cdlemk42  36229  dnnumch1  37614  aomclem3  37626  aomclem8  37631  dfac11  37632  dfacbasgrp  37678  ax6e2ndeq  38775  ax6e2ndeqVD  39145  fnchoice  39188  fiiuncl  39234  disjrnmpt2  39375  idlimc  39858  limcperiod  39860  limclner  39883  cnrefiisp  40056  climxlim2lem  40071  fperdvper  40133  stoweidlem35  40252  stoweidlem43  40260  stoweidlem59  40276  fourierdlem76  40399  etransclem47  40498  nnfoctbdjlem  40672  elprneb  41296  nrhmzr  41873