Theorem neeq1 2997

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  pm13.18  3016  pm13.181  3017  nelrdva  3653  psseq1  4028  n0snor2el  4771  0inp0  5294  nnullss  5408  opeqex  5446  frsn  5713  xp11  6133  limeq  6329  tz6.12i  6860  fveqressseq  7027  funopsnOLD  7098  fprg  7105  tpres  7152  f1dom3el3dif  7220  f1ounsn  7223  f1prex  7235  isofrlem  7291  resf1extb  7881  f1oweALT  7921  frxp  8073  xpord2lem  8089  poxp2  8090  frxp2  8091  xpord2indlem  8094  xpord3lem  8096  frxp3  8098  xpord3inddlem  8101  suppimacnv  8121  elqsn0  8728  frfi  9192  fiint  9234  marypha1lem  9343  frmin  9671  eldju2ndl  9846  dfac8alem  9949  dfac8clem  9952  aceq3lem  10040  dfac5lem3  10045  dfac5lem4  10046  dfac5lem4OLD  10048  dfac5  10049  dfac2b  10051  dfac9  10057  kmlem1  10071  kmlem12  10082  kmlem14  10084  fin2i  10215  isfin2-2  10239  fin23lem21  10259  fin1a2lem10  10329  axcc2lem  10356  dominf  10365  ac5b  10398  zornn0g  10425  axdclem  10439  dominfac  10494  elwina  10607  elina  10608  iswun  10625  rankcf  10698  axrrecex  11084  elimne0  11132  1re  11142  recex  11780  xnn0nemnf  12519  uzn0  12803  qreccl  12917  xrnemnf  13066  xrnepnf  13067  xnn0n0n1ge2b  13081  fztpval  13538  expcl2lem  14033  hashnemnf  14304  hashneq0  14324  hashge2el2difr  14441  hashdmpropge2  14443  relexp1g  14986  ntrivcvgn0  15861  ntrivcvgmullem  15864  fprodntriv  15905  divalglem7  16366  divalg  16370  gcdcllem1  16466  gcdcllem3  16468  pcpre1  16811  pcqmul  16822  pcqcl  16825  prmgaplem3  17022  prmgaplem4  17023  xpsfrnel  17524  mreintcl  17555  isdrs  18265  isipodrs  18501  sgrp2rid2ex  18896  frgpuptinv  19744  isnzr2  20497  nrhmzr  20516  isdrngrd  20745  isdrngrdOLD  20747  psgnodpmr  21572  lindfrn  21803  dmatelnd  22486  dmatmul  22487  mdetdiaglem  22588  mdetunilem1  22602  fvmptnn04ifa  22840  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  fiinopn  22891  hausnei  23318  dfconn2  23409  2ndcdisj  23446  regr1lem2  23730  isfbas  23819  ioorinv  25568  ioorcl  25569  vitalilem2  25601  vitalilem3  25602  vitali  25605  itg1climres  25706  mbfi1fseqlem4  25710  dvferm1lem  25976  dvferm2lem  25978  isuc1p  26131  ismon1p  26133  ply1remlem  26155  plydivlem4  26287  aannenlem1  26319  aannenlem2  26320  lgsne0  27323  lgsqr  27339  nolesgn2ores  27661  nogesgn1ores  27663  nosepdmlem  27672  nosupbnd1lem3  27699  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfbnd1lem3  27714  noinfbnd1lem5  27716  noinfbnd2lem1  27719  axtg5seg  28558  axtgupdim2  28564  axtgeucl  28565  axlowdim1  29053  lpvtx  29162  umgrnloopv  29200  usgrnloopvALT  29295  umgrvad2edg  29307  cusgrfilem2  29550  pthdlem2lem  29860  iswwlks  29929  iswwlksnx  29933  2pthdlem1  30023  isclwwlk  30079  3pthdlem1  30259  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupth2lem2  30314  eupth2lem3lem4  30326  eupth2lem3lem6  30328  3cyclfrgrrn1  30380  4cycl2vnunb  30385  frgrreg  30489  norm1exi  31346  shintcl  31426  chintcl  31428  chne0  31590  elspansn2  31663  eigre  31931  eigorth  31934  kbpj  32052  superpos  32450  hatomic  32456  isprmidl  33528  ismxidl  33552  ssmxidllem  33563  ssmxidl  33564  constrconj  33936  constrcccllem  33945  constrcbvlem  33946  2sqr3minply  33971  zarcmplem  34072  xrge0iifhom  34128  xrge0iif1  34129  esumpr2  34258  sibfof  34531  signswn0  34751  signswch  34752  signstfvneq0  34763  axtgupdim2ALTV  34859  bnj168  34920  bnj970  35136  bnj1154  35188  onvf1odlem2  35339  umgracycusgr  35389  cusgracyclt3v  35391  subfacp1lem1  35414  erdszelem8  35433  indispconn  35469  cvmsss2  35509  nepss  35953  elwlim  36056  dfrdg4  36186  fvray  36376  linedegen  36378  fvline  36379  hilbert1.1  36389  rankeq1o  36406  unblimceq0lem  36819  knoppndvlem21  36845  qdiff  37694  poimirlem1  37995  poimirlem17  38011  poimirlem20  38014  poimirlem32  38026  itg2addnclem3  38047  neificl  38127  isdrngo3  38333  ispridl  38408  ismaxidl  38414  islshp  39478  lsatn0  39498  lshpset2N  39618  atlex  39815  hlsuprexch  39880  3dimlem1  39957  llni2  40011  lplni2  40036  2llnjN  40066  lvoli2  40080  2lplnj  40119  islinei  40239  lnatexN  40278  llnexchb2  40368  lhpmatb  40530  cdleme40m  40966  cdlemftr3  41064  cdlemk28-3  41407  cdlemk35s  41436  cdlemk39s  41438  cdlemk42  41440  nnn1suc  42756  dnnumch1  43496  aomclem3  43508  aomclem8  43513  dfac11  43514  dfacbasgrp  43560  dfsucon  43974  ax6e2ndeq  45010  ax6e2ndeqVD  45359  relpfrlem  45404  permac8prim  45465  fnchoice  45484  fiiuncl  45520  disjrnmpt2  45642  idlimc  46078  limcperiod  46080  limclner  46101  cnrefiisp  46280  climxlim2lem  46295  fperdvper  46369  stoweidlem35  46485  stoweidlem43  46493  stoweidlem59  46509  fourierdlem76  46632  etransclem47  46731  nnfoctbdjlem  46905  elprneb  47499  ichexmpl1  47951  ichnreuop  47954  vopnbgrel  48352  dfclnbgr6  48354  dfnbgr6  48355  usgrgrtrirex  48448  isubgr3stgrlem4  48467  usgrexmpl2trifr  48535  gpg3kgrtriex  48587  itcoval2  49162  itcoval3  49163  itcovalsuc  49165  ackvalsuc1mpt  49176  inlinecirc02plem  49284  oppcthinendcALT  49938