Theorem neeq1 3000

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ne 2938

This theorem is referenced by:  pm13.18  3019  pm13.181  3020  nelrdva  3700  psseq1  4085  n0snor2el  4835  0inp0  5359  nnullss  5464  opeqex  5500  friOLD  5639  frsn  5765  xp11  6179  limeq  6381  tz6.12i  6925  fveqressseq  7089  funopsn  7157  fprg  7164  tpres  7213  f1dom3el3dif  7279  f1prex  7293  isofrlem  7348  f1oweALT  7976  frxp  8131  xpord2lem  8147  poxp2  8148  frxp2  8149  xpord2indlem  8152  xpord3lem  8154  frxp3  8156  xpord3inddlem  8159  suppimacnv  8179  elqsn0  8805  frfi  9313  fiint  9349  marypha1lem  9457  frmin  9773  eldju2ndl  9948  dfac8alem  10053  dfac8clem  10056  aceq3lem  10144  dfac5lem3  10149  dfac5lem4  10150  dfac5  10152  dfac2b  10154  dfac9  10160  kmlem1  10174  kmlem12  10185  kmlem14  10187  fin2i  10319  isfin2-2  10343  fin23lem21  10363  fin1a2lem10  10433  axcc2lem  10460  dominf  10469  ac5b  10502  zornn0g  10529  axdclem  10543  dominfac  10597  elwina  10710  elina  10711  iswun  10728  rankcf  10801  axrrecex  11187  elimne0  11235  1re  11245  recex  11877  xnn0nemnf  12586  uzn0  12870  qreccl  12984  xrnemnf  13130  xrnepnf  13131  xnn0n0n1ge2b  13144  fztpval  13596  expcl2lem  14071  hashnemnf  14336  hashneq0  14356  hashge2el2difr  14475  hashdmpropge2  14477  relexp1g  15006  ntrivcvgn0  15877  ntrivcvgmullem  15880  fprodntriv  15919  divalglem7  16376  divalg  16380  gcdcllem1  16474  gcdcllem3  16476  pcpre1  16811  pcqmul  16822  pcqcl  16825  prmgaplem3  17022  prmgaplem4  17023  xpsfrnel  17544  mreintcl  17575  isdrs  18293  isipodrs  18529  sgrp2rid2ex  18879  frgpuptinv  19726  isnzr2  20457  nrhmzr  20474  isdrngrd  20658  isdrngrdOLD  20660  psgnodpmr  21522  lindfrn  21755  dmatelnd  22411  dmatmul  22412  mdetdiaglem  22513  mdetunilem1  22527  fvmptnn04ifa  22765  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  fiinopn  22816  hausnei  23245  dfconn2  23336  2ndcdisj  23373  regr1lem2  23657  isfbas  23746  ioorinv  25518  ioorcl  25519  vitalilem2  25551  vitalilem3  25552  vitali  25555  itg1climres  25657  mbfi1fseqlem4  25661  dvferm1lem  25929  dvferm2lem  25931  isuc1p  26089  ismon1p  26091  ply1remlem  26112  plydivlem4  26244  aannenlem1  26276  aannenlem2  26277  lgsne0  27281  lgsqr  27297  nolesgn2ores  27618  nogesgn1ores  27620  nosepdmlem  27629  nosupbnd1lem3  27656  nosupbnd1lem5  27658  nosupbnd2lem1  27661  noinfbnd1lem3  27671  noinfbnd1lem5  27673  noinfbnd2lem1  27676  axtg5seg  28282  axtgupdim2  28288  axtgeucl  28289  axlowdim1  28783  lpvtx  28894  umgrnloopv  28932  usgrnloopvALT  29027  umgrvad2edg  29039  cusgrfilem2  29283  pthdlem2lem  29594  iswwlks  29660  iswwlksnx  29664  2pthdlem1  29754  isclwwlk  29807  3pthdlem1  29987  upgr3v3e3cycl  30003  upgr4cycl4dv4e  30008  eupth2lem2  30042  eupth2lem3lem4  30054  eupth2lem3lem6  30056  3cyclfrgrrn1  30108  4cycl2vnunb  30113  frgrreg  30217  norm1exi  31073  shintcl  31153  chintcl  31155  chne0  31317  elspansn2  31390  eigre  31658  eigorth  31661  kbpj  31779  superpos  32177  hatomic  32183  isprmidl  33167  ismxidl  33188  ssmxidllem  33199  ssmxidl  33200  zarcmplem  33482  xrge0iifhom  33538  xrge0iif1  33539  esumpr2  33686  sibfof  33960  signswn0  34192  signswch  34193  signstfvneq0  34204  axtgupdim2ALTV  34300  bnj168  34361  bnj970  34578  bnj1154  34630  umgracycusgr  34764  cusgracyclt3v  34766  subfacp1lem1  34789  erdszelem8  34808  indispconn  34844  cvmsss2  34884  nepss  35312  elwlim  35419  dfrdg4  35547  fvray  35737  linedegen  35739  fvline  35740  hilbert1.1  35750  rankeq1o  35767  unblimceq0lem  35981  knoppndvlem21  36007  poimirlem1  37094  poimirlem17  37110  poimirlem20  37113  poimirlem32  37125  itg2addnclem3  37146  neificl  37226  isdrngo3  37432  ispridl  37507  ismaxidl  37513  islshp  38451  lsatn0  38471  lshpset2N  38591  atlex  38788  hlsuprexch  38854  3dimlem1  38931  llni2  38985  lplni2  39010  2llnjN  39040  lvoli2  39054  2lplnj  39093  islinei  39213  lnatexN  39252  llnexchb2  39342  lhpmatb  39504  cdleme40m  39940  cdlemftr3  40038  cdlemk28-3  40381  cdlemk35s  40410  cdlemk39s  40412  cdlemk42  40414  metakunt30  41686  nnn1suc  41841  dnnumch1  42468  aomclem3  42480  aomclem8  42485  dfac11  42486  dfacbasgrp  42532  dfsucon  42953  ax6e2ndeq  43998  ax6e2ndeqVD  44348  fnchoice  44391  fiiuncl  44429  disjrnmpt2  44561  idlimc  45014  limcperiod  45016  limclner  45039  cnrefiisp  45218  climxlim2lem  45233  fperdvper  45307  stoweidlem35  45423  stoweidlem43  45431  stoweidlem59  45447  fourierdlem76  45570  etransclem47  45669  nnfoctbdjlem  45843  elprneb  46411  ichexmpl1  46809  ichnreuop  46812  itcoval2  47737  itcoval3  47738  itcovalsuc  47740  ackvalsuc1mpt  47751  inlinecirc02plem  47859