Theorem neeq1 2987

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 2984	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  pm13.18  3006  pm13.181  3007  nelrdva  3667  psseq1  4043  n0snor2el  4787  0inp0  5301  nnullss  5409  opeqex  5445  frsn  5711  xp11  6128  limeq  6323  tz6.12i  6852  fveqressseq  7017  funopsn  7086  fprg  7093  tpres  7141  f1dom3el3dif  7210  f1ounsn  7213  f1prex  7225  isofrlem  7281  resf1extb  7874  f1oweALT  7914  frxp  8066  xpord2lem  8082  poxp2  8083  frxp2  8084  xpord2indlem  8087  xpord3lem  8089  frxp3  8091  xpord3inddlem  8094  suppimacnv  8114  elqsn0  8718  frfi  9190  fiint  9235  fiintOLD  9236  marypha1lem  9342  frmin  9664  eldju2ndl  9839  dfac8alem  9942  dfac8clem  9945  aceq3lem  10033  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  dfac9  10050  kmlem1  10064  kmlem12  10075  kmlem14  10077  fin2i  10208  isfin2-2  10232  fin23lem21  10252  fin1a2lem10  10322  axcc2lem  10349  dominf  10358  ac5b  10391  zornn0g  10418  axdclem  10432  dominfac  10486  elwina  10599  elina  10600  iswun  10617  rankcf  10690  axrrecex  11076  elimne0  11124  1re  11134  recex  11770  xnn0nemnf  12486  uzn0  12770  qreccl  12888  xrnemnf  13037  xrnepnf  13038  xnn0n0n1ge2b  13052  fztpval  13507  expcl2lem  13998  hashnemnf  14269  hashneq0  14289  hashge2el2difr  14406  hashdmpropge2  14408  relexp1g  14951  ntrivcvgn0  15823  ntrivcvgmullem  15826  fprodntriv  15867  divalglem7  16328  divalg  16332  gcdcllem1  16428  gcdcllem3  16430  pcpre1  16772  pcqmul  16783  pcqcl  16786  prmgaplem3  16983  prmgaplem4  16984  xpsfrnel  17484  mreintcl  17515  isdrs  18225  isipodrs  18461  sgrp2rid2ex  18819  frgpuptinv  19668  isnzr2  20421  nrhmzr  20440  isdrngrd  20669  isdrngrdOLD  20671  psgnodpmr  21515  lindfrn  21746  dmatelnd  22399  dmatmul  22400  mdetdiaglem  22501  mdetunilem1  22515  fvmptnn04ifa  22753  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  fiinopn  22804  hausnei  23231  dfconn2  23322  2ndcdisj  23359  regr1lem2  23643  isfbas  23732  ioorinv  25493  ioorcl  25494  vitalilem2  25526  vitalilem3  25527  vitali  25530  itg1climres  25631  mbfi1fseqlem4  25635  dvferm1lem  25904  dvferm2lem  25906  isuc1p  26062  ismon1p  26064  ply1remlem  26086  plydivlem4  26220  aannenlem1  26252  aannenlem2  26253  lgsne0  27262  lgsqr  27278  nolesgn2ores  27600  nogesgn1ores  27602  nosepdmlem  27611  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  axtg5seg  28428  axtgupdim2  28434  axtgeucl  28435  axlowdim1  28922  lpvtx  29031  umgrnloopv  29069  usgrnloopvALT  29164  umgrvad2edg  29176  cusgrfilem2  29420  pthdlem2lem  29730  iswwlks  29799  iswwlksnx  29803  2pthdlem1  29893  isclwwlk  29946  3pthdlem1  30126  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth2lem2  30181  eupth2lem3lem4  30193  eupth2lem3lem6  30195  3cyclfrgrrn1  30247  4cycl2vnunb  30252  frgrreg  30356  norm1exi  31212  shintcl  31292  chintcl  31294  chne0  31456  elspansn2  31529  eigre  31797  eigorth  31800  kbpj  31918  superpos  32316  hatomic  32322  isprmidl  33388  ismxidl  33412  ssmxidllem  33423  ssmxidl  33424  constrconj  33714  constrcccllem  33723  constrcbvlem  33724  2sqr3minply  33749  zarcmplem  33850  xrge0iifhom  33906  xrge0iif1  33907  esumpr2  34036  sibfof  34310  signswn0  34530  signswch  34531  signstfvneq0  34542  axtgupdim2ALTV  34638  bnj168  34699  bnj970  34916  bnj1154  34968  onvf1odlem2  35079  umgracycusgr  35129  cusgracyclt3v  35131  subfacp1lem1  35154  erdszelem8  35173  indispconn  35209  cvmsss2  35249  nepss  35693  elwlim  35799  dfrdg4  35927  fvray  36117  linedegen  36119  fvline  36120  hilbert1.1  36130  rankeq1o  36147  unblimceq0lem  36482  knoppndvlem21  36508  poimirlem1  37603  poimirlem17  37619  poimirlem20  37622  poimirlem32  37634  itg2addnclem3  37655  neificl  37735  isdrngo3  37941  ispridl  38016  ismaxidl  38022  islshp  38960  lsatn0  38980  lshpset2N  39100  atlex  39297  hlsuprexch  39363  3dimlem1  39440  llni2  39494  lplni2  39519  2llnjN  39549  lvoli2  39563  2lplnj  39602  islinei  39722  lnatexN  39761  llnexchb2  39851  lhpmatb  40013  cdleme40m  40449  cdlemftr3  40547  cdlemk28-3  40890  cdlemk35s  40919  cdlemk39s  40921  cdlemk42  40923  nnn1suc  42242  dnnumch1  43020  aomclem3  43032  aomclem8  43037  dfac11  43038  dfacbasgrp  43084  dfsucon  43499  ax6e2ndeq  44536  ax6e2ndeqVD  44885  relpfrlem  44930  permac8prim  44991  fnchoice  45010  fiiuncl  45046  disjrnmpt2  45169  idlimc  45611  limcperiod  45613  limclner  45636  cnrefiisp  45815  climxlim2lem  45830  fperdvper  45904  stoweidlem35  46020  stoweidlem43  46028  stoweidlem59  46044  fourierdlem76  46167  etransclem47  46266  nnfoctbdjlem  46440  elprneb  47017  ichexmpl1  47457  ichnreuop  47460  vopnbgrel  47842  dfclnbgr6  47844  dfnbgr6  47845  usgrgrtrirex  47938  isubgr3stgrlem4  47957  usgrexmpl2trifr  48025  gpg3kgrtriex  48077  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  inlinecirc02plem  48775  oppcthinendcALT  49430