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  3676  psseq1  4053  n0snor2el  4797  0inp0  5314  nnullss  5422  opeqex  5458  frsn  5726  xp11  6148  limeq  6344  tz6.12i  6886  fveqressseq  7051  funopsn  7120  fprg  7127  tpres  7175  f1dom3el3dif  7244  f1ounsn  7247  f1prex  7259  isofrlem  7315  resf1extb  7910  f1oweALT  7951  frxp  8105  xpord2lem  8121  poxp2  8122  frxp2  8123  xpord2indlem  8126  xpord3lem  8128  frxp3  8130  xpord3inddlem  8133  suppimacnv  8153  elqsn0  8757  frfi  9232  fiint  9277  fiintOLD  9278  marypha1lem  9384  frmin  9702  eldju2ndl  9877  dfac8alem  9982  dfac8clem  9985  aceq3lem  10073  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  dfac5  10082  dfac2b  10084  dfac9  10090  kmlem1  10104  kmlem12  10115  kmlem14  10117  fin2i  10248  isfin2-2  10272  fin23lem21  10292  fin1a2lem10  10362  axcc2lem  10389  dominf  10398  ac5b  10431  zornn0g  10458  axdclem  10472  dominfac  10526  elwina  10639  elina  10640  iswun  10657  rankcf  10730  axrrecex  11116  elimne0  11164  1re  11174  recex  11810  xnn0nemnf  12526  uzn0  12810  qreccl  12928  xrnemnf  13077  xrnepnf  13078  xnn0n0n1ge2b  13092  fztpval  13547  expcl2lem  14038  hashnemnf  14309  hashneq0  14329  hashge2el2difr  14446  hashdmpropge2  14448  relexp1g  14992  ntrivcvgn0  15864  ntrivcvgmullem  15867  fprodntriv  15908  divalglem7  16369  divalg  16373  gcdcllem1  16469  gcdcllem3  16471  pcpre1  16813  pcqmul  16824  pcqcl  16827  prmgaplem3  17024  prmgaplem4  17025  xpsfrnel  17525  mreintcl  17556  isdrs  18262  isipodrs  18496  sgrp2rid2ex  18854  frgpuptinv  19701  isnzr2  20427  nrhmzr  20446  isdrngrd  20675  isdrngrdOLD  20677  psgnodpmr  21499  lindfrn  21730  dmatelnd  22383  dmatmul  22384  mdetdiaglem  22485  mdetunilem1  22499  fvmptnn04ifa  22737  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  fiinopn  22788  hausnei  23215  dfconn2  23306  2ndcdisj  23343  regr1lem2  23627  isfbas  23716  ioorinv  25477  ioorcl  25478  vitalilem2  25510  vitalilem3  25511  vitali  25514  itg1climres  25615  mbfi1fseqlem4  25619  dvferm1lem  25888  dvferm2lem  25890  isuc1p  26046  ismon1p  26048  ply1remlem  26070  plydivlem4  26204  aannenlem1  26236  aannenlem2  26237  lgsne0  27246  lgsqr  27262  nolesgn2ores  27584  nogesgn1ores  27586  nosepdmlem  27595  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  axlowdim1  28886  lpvtx  28995  umgrnloopv  29033  usgrnloopvALT  29128  umgrvad2edg  29140  cusgrfilem2  29384  pthdlem2lem  29697  iswwlks  29766  iswwlksnx  29770  2pthdlem1  29860  isclwwlk  29913  3pthdlem1  30093  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eupth2lem2  30148  eupth2lem3lem4  30160  eupth2lem3lem6  30162  3cyclfrgrrn1  30214  4cycl2vnunb  30219  frgrreg  30323  norm1exi  31179  shintcl  31259  chintcl  31261  chne0  31423  elspansn2  31496  eigre  31764  eigorth  31767  kbpj  31885  superpos  32283  hatomic  32289  isprmidl  33409  ismxidl  33433  ssmxidllem  33444  ssmxidl  33445  constrconj  33735  constrcccllem  33744  constrcbvlem  33745  2sqr3minply  33770  zarcmplem  33871  xrge0iifhom  33927  xrge0iif1  33928  esumpr2  34057  sibfof  34331  signswn0  34551  signswch  34552  signstfvneq0  34563  axtgupdim2ALTV  34659  bnj168  34720  bnj970  34937  bnj1154  34989  onvf1odlem2  35091  umgracycusgr  35141  cusgracyclt3v  35143  subfacp1lem1  35166  erdszelem8  35185  indispconn  35221  cvmsss2  35261  nepss  35705  elwlim  35811  dfrdg4  35939  fvray  36129  linedegen  36131  fvline  36132  hilbert1.1  36142  rankeq1o  36159  unblimceq0lem  36494  knoppndvlem21  36520  poimirlem1  37615  poimirlem17  37631  poimirlem20  37634  poimirlem32  37646  itg2addnclem3  37667  neificl  37747  isdrngo3  37953  ispridl  38028  ismaxidl  38034  islshp  38972  lsatn0  38992  lshpset2N  39112  atlex  39309  hlsuprexch  39375  3dimlem1  39452  llni2  39506  lplni2  39531  2llnjN  39561  lvoli2  39575  2lplnj  39614  islinei  39734  lnatexN  39773  llnexchb2  39863  lhpmatb  40025  cdleme40m  40461  cdlemftr3  40559  cdlemk28-3  40902  cdlemk35s  40931  cdlemk39s  40933  cdlemk42  40935  nnn1suc  42254  dnnumch1  43033  aomclem3  43045  aomclem8  43050  dfac11  43051  dfacbasgrp  43097  dfsucon  43512  ax6e2ndeq  44549  ax6e2ndeqVD  44898  relpfrlem  44943  permac8prim  45004  fnchoice  45023  fiiuncl  45059  disjrnmpt2  45182  idlimc  45624  limcperiod  45626  limclner  45649  cnrefiisp  45828  climxlim2lem  45843  fperdvper  45917  stoweidlem35  46033  stoweidlem43  46041  stoweidlem59  46057  fourierdlem76  46180  etransclem47  46279  nnfoctbdjlem  46453  elprneb  47030  ichexmpl1  47470  ichnreuop  47473  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  usgrgrtrirex  47949  isubgr3stgrlem4  47968  usgrexmpl2trifr  48028  gpg3kgrtriex  48080  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  inlinecirc02plem  48775  oppcthinendcALT  49430