Theorem neeq1 2995

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

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

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 2708

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

This theorem is referenced by:  pm13.18  3014  pm13.181  3015  nelrdva  3693  psseq1  4070  n0snor2el  4814  0inp0  5334  nnullss  5442  opeqex  5478  friOLD  5617  frsn  5747  xp11  6169  limeq  6369  tz6.12i  6909  fveqressseq  7074  funopsn  7143  fprg  7150  tpres  7198  f1dom3el3dif  7267  f1ounsn  7270  f1prex  7282  isofrlem  7338  resf1extb  7935  f1oweALT  7976  frxp  8130  xpord2lem  8146  poxp2  8147  frxp2  8148  xpord2indlem  8151  xpord3lem  8153  frxp3  8155  xpord3inddlem  8158  suppimacnv  8178  elqsn0  8805  frfi  9298  fiint  9343  fiintOLD  9344  marypha1lem  9450  frmin  9768  eldju2ndl  9943  dfac8alem  10048  dfac8clem  10051  aceq3lem  10139  dfac5lem3  10144  dfac5lem4  10145  dfac5lem4OLD  10147  dfac5  10148  dfac2b  10150  dfac9  10156  kmlem1  10170  kmlem12  10181  kmlem14  10183  fin2i  10314  isfin2-2  10338  fin23lem21  10358  fin1a2lem10  10428  axcc2lem  10455  dominf  10464  ac5b  10497  zornn0g  10524  axdclem  10538  dominfac  10592  elwina  10705  elina  10706  iswun  10723  rankcf  10796  axrrecex  11182  elimne0  11230  1re  11240  recex  11874  xnn0nemnf  12590  uzn0  12874  qreccl  12990  xrnemnf  13138  xrnepnf  13139  xnn0n0n1ge2b  13153  fztpval  13608  expcl2lem  14096  hashnemnf  14367  hashneq0  14387  hashge2el2difr  14504  hashdmpropge2  14506  relexp1g  15050  ntrivcvgn0  15919  ntrivcvgmullem  15922  fprodntriv  15963  divalglem7  16423  divalg  16427  gcdcllem1  16523  gcdcllem3  16525  pcpre1  16867  pcqmul  16878  pcqcl  16881  prmgaplem3  17078  prmgaplem4  17079  xpsfrnel  17581  mreintcl  17612  isdrs  18318  isipodrs  18552  sgrp2rid2ex  18910  frgpuptinv  19757  isnzr2  20483  nrhmzr  20502  isdrngrd  20731  isdrngrdOLD  20733  psgnodpmr  21555  lindfrn  21786  dmatelnd  22439  dmatmul  22440  mdetdiaglem  22541  mdetunilem1  22555  fvmptnn04ifa  22793  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  fiinopn  22844  hausnei  23271  dfconn2  23362  2ndcdisj  23399  regr1lem2  23683  isfbas  23772  ioorinv  25534  ioorcl  25535  vitalilem2  25567  vitalilem3  25568  vitali  25571  itg1climres  25672  mbfi1fseqlem4  25676  dvferm1lem  25945  dvferm2lem  25947  isuc1p  26103  ismon1p  26105  ply1remlem  26127  plydivlem4  26261  aannenlem1  26293  aannenlem2  26294  lgsne0  27303  lgsqr  27319  nolesgn2ores  27641  nogesgn1ores  27643  nosepdmlem  27652  nosupbnd1lem3  27679  nosupbnd1lem5  27681  nosupbnd2lem1  27684  noinfbnd1lem3  27694  noinfbnd1lem5  27696  noinfbnd2lem1  27699  axtg5seg  28449  axtgupdim2  28455  axtgeucl  28456  axlowdim1  28943  lpvtx  29052  umgrnloopv  29090  usgrnloopvALT  29185  umgrvad2edg  29197  cusgrfilem2  29441  pthdlem2lem  29754  iswwlks  29823  iswwlksnx  29827  2pthdlem1  29917  isclwwlk  29970  3pthdlem1  30150  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  eupth2lem2  30205  eupth2lem3lem4  30217  eupth2lem3lem6  30219  3cyclfrgrrn1  30271  4cycl2vnunb  30276  frgrreg  30380  norm1exi  31236  shintcl  31316  chintcl  31318  chne0  31480  elspansn2  31553  eigre  31821  eigorth  31824  kbpj  31942  superpos  32340  hatomic  32346  isprmidl  33458  ismxidl  33482  ssmxidllem  33493  ssmxidl  33494  constrconj  33784  constrcccllem  33793  constrcbvlem  33794  2sqr3minply  33819  zarcmplem  33917  xrge0iifhom  33973  xrge0iif1  33974  esumpr2  34103  sibfof  34377  signswn0  34597  signswch  34598  signstfvneq0  34609  axtgupdim2ALTV  34705  bnj168  34766  bnj970  34983  bnj1154  35035  umgracycusgr  35181  cusgracyclt3v  35183  subfacp1lem1  35206  erdszelem8  35225  indispconn  35261  cvmsss2  35301  nepss  35740  elwlim  35846  dfrdg4  35974  fvray  36164  linedegen  36166  fvline  36167  hilbert1.1  36177  rankeq1o  36194  unblimceq0lem  36529  knoppndvlem21  36555  poimirlem1  37650  poimirlem17  37666  poimirlem20  37669  poimirlem32  37681  itg2addnclem3  37702  neificl  37782  isdrngo3  37988  ispridl  38063  ismaxidl  38069  islshp  39002  lsatn0  39022  lshpset2N  39142  atlex  39339  hlsuprexch  39405  3dimlem1  39482  llni2  39536  lplni2  39561  2llnjN  39591  lvoli2  39605  2lplnj  39644  islinei  39764  lnatexN  39803  llnexchb2  39893  lhpmatb  40055  cdleme40m  40491  cdlemftr3  40589  cdlemk28-3  40932  cdlemk35s  40961  cdlemk39s  40963  cdlemk42  40965  nnn1suc  42284  dnnumch1  43043  aomclem3  43055  aomclem8  43060  dfac11  43061  dfacbasgrp  43107  dfsucon  43522  ax6e2ndeq  44559  ax6e2ndeqVD  44908  relpfrlem  44953  permac8prim  45014  fnchoice  45033  fiiuncl  45069  disjrnmpt2  45192  idlimc  45635  limcperiod  45637  limclner  45660  cnrefiisp  45839  climxlim2lem  45854  fperdvper  45928  stoweidlem35  46044  stoweidlem43  46052  stoweidlem59  46068  fourierdlem76  46191  etransclem47  46290  nnfoctbdjlem  46464  elprneb  47038  ichexmpl1  47463  ichnreuop  47466  vopnbgrel  47847  dfclnbgr6  47849  dfnbgr6  47850  usgrgrtrirex  47942  isubgr3stgrlem4  47961  usgrexmpl2trifr  48021  gpg3kgrtriex  48071  itcoval2  48624  itcoval3  48625  itcovalsuc  48627  ackvalsuc1mpt  48638  inlinecirc02plem  48746  oppcthinendcALT  49307