Theorem neeq1 2738

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1395   =/= wne 2652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654

This theorem is referenced by:  neeq1iOLD  2743  neeq1dOLD  2748  nelrdva  3309  psseq1  3587  0inp0  4628  nnullss  4718  opeqex  4747  fri  4850  limeq  4899  xp11  5449  tz6.12i  5892  fveqressseq  6028  fprg  6081  tpres  6125  f1dom3el3dif  6177  isofrlem  6237  f1oweALT  6783  frxp  6909  suppimacnv  6928  elqsn0  7398  frfi  7783  fiint  7815  marypha1lem  7911  dfac8alem  8427  dfac8clem  8430  aceq3lem  8518  dfac5lem3  8523  dfac5lem4  8524  dfac5  8526  dfac2  8528  dfac9  8533  kmlem1  8547  kmlem12  8558  kmlem14  8560  fin2i  8692  isfin2-2  8716  fin23lem21  8736  fin1a2lem10  8806  axcc2lem  8833  dominf  8842  ac5b  8875  zornn0g  8902  axdclem  8916  dominfac  8965  elwina  9081  elina  9082  iswun  9099  rankcf  9172  axrrecex  9557  elimne0  9603  1re  9612  recex  10202  uzn0  11121  qreccl  11227  xrnemnf  11353  xrnepnf  11354  fztpval  11767  expcl2lem  12181  hashnemnf  12420  hashneq0  12437  ntrivcvgn0  13719  ntrivcvgmullem  13722  fprodntriv  13761  divalglem7  14069  divalg  14073  gcdcllem1  14161  gcdcllem3  14163  isprm2lem  14236  pcpre1  14378  pcqmul  14389  pcqcl  14392  xpscfv  14979  xpsfrnel  14980  mreintcl  15012  isdrs  15690  isipodrs  15918  sgrp2rid2ex  16172  frgpuptinv  16916  isdrngrd  17549  isnzr2  18038  psgnodpmr  18753  lindfrn  18983  dmatelnd  19125  dmatmul  19126  mdetdiaglem  19227  mdetunilem1  19241  fvmptnn04ifa  19478  chfacfscmulgsum  19488  chfacfpmmulgsum  19492  fiinopn  19537  hausnei  19956  dfcon2  20046  2ndcdisj  20083  regr1lem2  20367  isfbas  20456  ioorinv  22111  ioorcl  22112  vitalilem2  22144  vitalilem3  22145  vitali  22148  itg1climres  22247  mbfi1fseqlem4  22251  dvferm1lem  22511  dvferm2lem  22513  isuc1p  22667  ismon1p  22669  ply1remlem  22689  plydivlem4  22818  aannenlem1  22850  aannenlem2  22851  lgsne0  23734  lgsqr  23747  axtg5seg  23988  axtgupdim2  23995  axtgeucl  23996  axlowdim1  24389  usgranloopv  24505  usgra1v  24517  cusgrafilem2  24607  wlkn0  24654  2pthoncl  24732  iswwlk  24810  eupath2lem2  25105  eupath2lem3  25106  3cyclfrgrarn1  25139  4cycl2vnunb  25144  frgrawopreglem3  25173  norm1exi  26295  shintcl  26375  chintcl  26377  chne0  26539  elspansn2  26612  eigre  26881  eigorth  26884  kbpj  27002  superpos  27400  hatomic  27406  xrge0iifhom  28080  xrge0iif1  28081  esumpr2  28239  sibfof  28479  signswn0  28714  signswch  28715  signstfvneq0  28726  subfacp1lem1  28820  erdszelem8  28839  indispcon  28876  cvmsss2  28916  relexp1g  29253  nepss  29313  frmin  29539  elwlim  29596  dfrdg4  29805  fvray  29996  linedegen  29998  fvline  29999  hilbert1.1  30009  rankeq1o  30033  itg2addnclem3  30273  neificl  30451  isdrngo3  30567  ispridl  30636  ismaxidl  30642  dnnumch1  31194  aomclem3  31206  aomclem8  31211  dfac11  31212  dfacbasgrp  31261  fnchoice  31607  idlimc  31835  limcperiod  31837  limclner  31860  fperdvper  31918  stoweidlem35  32020  stoweidlem43  32028  stoweidlem59  32044  fourierdlem76  32168  etransclem47  32267  usgvad2edg  32673  nrhmzr  32823  ax6e2ndeq  33475  ax6e2ndeqVD  33852  bnj168  33928  bnj970  34148  bnj1154  34198  islshp  34847  lsatn0  34867  lshpset2N  34987  atlex  35184  hlsuprexch  35248  3dimlem1  35325  llni2  35379  lplni2  35404  2llnjN  35434  lvoli2  35448  2lplnj  35487  islinei  35607  lnatexN  35646  llnexchb2  35736  lhpmatb  35898  cdleme40m  36336  cdlemftr3  36434  cdlemk28-3  36777  cdlemk35s  36806  cdlemk39s  36808  cdlemk42  36810