Theorem neeq1 2844

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

Assertion

Ref	Expression
neeq1	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq1d 2841	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  nelrdva  3384  psseq1  3656  n0snor2el  4304  0inp0  4763  nnullss  4857  opeqex  4887  fri  5000  frsn  5112  xp11  5488  limeq  5652  tz6.12i  6124  fveqressseq  6263  funopsn  6319  fprg  6327  tpres  6371  f1dom3el3dif  6426  f1prex  6439  isofrlem  6490  f1oweALT  7043  frxp  7174  suppimacnv  7193  elqsn0  7703  frfi  8090  fiint  8122  marypha1lem  8222  dfac8alem  8735  dfac8clem  8738  aceq3lem  8826  dfac5lem3  8831  dfac5lem4  8832  dfac5  8834  dfac2  8836  dfac9  8841  kmlem1  8855  kmlem12  8866  kmlem14  8868  fin2i  9000  isfin2-2  9024  fin23lem21  9044  fin1a2lem10  9114  axcc2lem  9141  dominf  9150  ac5b  9183  zornn0g  9210  axdclem  9224  dominfac  9274  elwina  9387  elina  9388  iswun  9405  rankcf  9478  axrrecex  9863  elimne0  9909  1re  9918  recex  10538  xnn0nemnf  11251  uzn0  11579  qreccl  11684  xrnemnf  11827  xrnepnf  11828  xnn0n0n1ge2b  11841  fztpval  12272  expcl2lem  12734  hashnemnf  12994  hashneq0  13016  hashge2el2difr  13118  relexp1g  13614  ntrivcvgn0  14469  ntrivcvgmullem  14472  fprodntriv  14511  divalglem7  14960  divalg  14964  gcdcllem1  15059  gcdcllem3  15061  isprm2lem  15232  pcpre1  15385  pcqmul  15396  pcqcl  15399  prmgaplem3  15595  prmgaplem4  15596  xpscfv  16045  xpsfrnel  16046  mreintcl  16078  isdrs  16757  isipodrs  16984  sgrp2rid2ex  17237  frgpuptinv  18007  isdrngrd  18596  isnzr2  19084  psgnodpmr  19755  lindfrn  19979  dmatelnd  20121  dmatmul  20122  mdetdiaglem  20223  mdetunilem1  20237  fvmptnn04ifa  20474  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  fiinopn  20531  hausnei  20942  dfcon2  21032  2ndcdisj  21069  regr1lem2  21353  isfbas  21443  ioorinv  23150  ioorcl  23151  vitalilem2  23184  vitalilem3  23185  vitali  23188  itg1climres  23287  mbfi1fseqlem4  23291  dvferm1lem  23551  dvferm2lem  23553  isuc1p  23704  ismon1p  23706  ply1remlem  23726  plydivlem4  23855  aannenlem1  23887  aannenlem2  23888  lgsne0  24860  lgsqr  24876  axtg5seg  25164  axtgupdim2  25170  axtgeucl  25171  axlowdim1  25639  structgrssvtxlem  25700  lpvtx  25734  umgrnloopv  25772  usgranloopv  25907  usgra1v  25919  cusgrafilem2  26008  wlkn0  26055  2pthoncl  26133  iswwlk  26211  eupath2lem2  26505  eupath2lem3  26506  3cyclfrgrarn1  26539  4cycl2vnunb  26544  frgrawopreglem3  26573  norm1exi  27491  shintcl  27573  chintcl  27575  chne0  27737  elspansn2  27810  eigre  28078  eigorth  28081  kbpj  28199  superpos  28597  hatomic  28603  xrge0iifhom  29311  xrge0iif1  29312  esumpr2  29456  sibfof  29729  signswn0  29963  signswch  29964  signstfvneq0  29975  axtgupdim2OLD  29999  bnj168  30052  bnj970  30271  bnj1154  30321  subfacp1lem1  30415  erdszelem8  30434  indispcon  30470  cvmsss2  30510  nepss  30854  frmin  30983  elwlim  31013  elwlimOLD  31014  dfrdg4  31228  fvray  31418  linedegen  31420  fvline  31421  hilbert1.1  31431  rankeq1o  31448  unblimceq0lem  31667  knoppndvlem21  31693  poimirlem1  32580  poimirlem17  32596  poimirlem20  32599  poimirlem32  32611  itg2addnclem3  32633  neificl  32719  isdrngo3  32928  ispridl  33003  ismaxidl  33009  islshp  33284  lsatn0  33304  lshpset2N  33424  atlex  33621  hlsuprexch  33685  3dimlem1  33762  llni2  33816  lplni2  33841  2llnjN  33871  lvoli2  33885  2lplnj  33924  islinei  34044  lnatexN  34083  llnexchb2  34173  lhpmatb  34335  cdleme40m  34773  cdlemftr3  34871  cdlemk28-3  35214  cdlemk35s  35243  cdlemk39s  35245  cdlemk42  35247  dnnumch1  36632  aomclem3  36644  aomclem8  36649  dfac11  36650  dfacbasgrp  36697  ax6e2ndeq  37796  ax6e2ndeqVD  38167  fnchoice  38211  fiiuncl  38259  disjrnmpt2  38370  idlimc  38693  limcperiod  38695  limclner  38718  fperdvper  38808  stoweidlem35  38928  stoweidlem43  38936  stoweidlem59  38952  fourierdlem76  39075  etransclem47  39174  nnfoctbdjlem  39348  elprneb  39939  usgrnloopvALT  40428  umgrvad2edg  40440  cusgrfilem2  40672  pthdlem2lem  40973  iswwlks  41039  iswwlksnx  41042  2pthdlem1  41137  isclwwlks  41188  3pthdlem1  41331  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupth2lem2  41387  eupth2lem3lem4  41399  eupth2lem3lem6  41401  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  frgrwopreglem3  41483  av-frgrareg  41548  nrhmzr  41663  ssdifsn  42228