Theorem neeq1 2994

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  pm13.18  3013  pm13.181  3014  nelrdva  3651  psseq1  4030  n0snor2el  4776  0inp0  5300  nnullss  5414  opeqex  5452  frsn  5719  xp11  6139  limeq  6335  tz6.12i  6866  fveqressseq  7031  funopsnOLD  7102  fprg  7109  tpres  7156  f1dom3el3dif  7224  f1ounsn  7227  f1prex  7239  isofrlem  7295  resf1extb  7885  f1oweALT  7925  frxp  8076  xpord2lem  8092  poxp2  8093  frxp2  8094  xpord2indlem  8097  xpord3lem  8099  frxp3  8101  xpord3inddlem  8104  suppimacnv  8124  elqsn0  8731  frfi  9195  fiint  9237  marypha1lem  9346  frmin  9673  eldju2ndl  9848  dfac8alem  9951  dfac8clem  9954  aceq3lem  10042  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  dfac9  10059  kmlem1  10073  kmlem12  10084  kmlem14  10086  fin2i  10217  isfin2-2  10241  fin23lem21  10261  fin1a2lem10  10331  axcc2lem  10358  dominf  10367  ac5b  10400  zornn0g  10427  axdclem  10441  dominfac  10496  elwina  10609  elina  10610  iswun  10627  rankcf  10700  axrrecex  11086  elimne0  11134  1re  11144  recex  11782  xnn0nemnf  12521  uzn0  12805  qreccl  12919  xrnemnf  13068  xrnepnf  13069  xnn0n0n1ge2b  13083  fztpval  13540  expcl2lem  14035  hashnemnf  14306  hashneq0  14326  hashge2el2difr  14443  hashdmpropge2  14445  relexp1g  14988  ntrivcvgn0  15863  ntrivcvgmullem  15866  fprodntriv  15907  divalglem7  16368  divalg  16372  gcdcllem1  16468  gcdcllem3  16470  pcpre1  16813  pcqmul  16824  pcqcl  16827  prmgaplem3  17024  prmgaplem4  17025  xpsfrnel  17526  mreintcl  17557  isdrs  18267  isipodrs  18503  sgrp2rid2ex  18898  frgpuptinv  19746  isnzr2  20495  nrhmzr  20514  isdrngrd  20743  isdrngrdOLD  20745  psgnodpmr  21570  lindfrn  21801  dmatelnd  22461  dmatmul  22462  mdetdiaglem  22563  mdetunilem1  22577  fvmptnn04ifa  22815  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  fiinopn  22866  hausnei  23293  dfconn2  23384  2ndcdisj  23421  regr1lem2  23705  isfbas  23794  ioorinv  25543  ioorcl  25544  vitalilem2  25576  vitalilem3  25577  vitali  25580  itg1climres  25681  mbfi1fseqlem4  25685  dvferm1lem  25951  dvferm2lem  25953  isuc1p  26106  ismon1p  26108  ply1remlem  26130  plydivlem4  26262  aannenlem1  26294  aannenlem2  26295  lgsne0  27298  lgsqr  27314  nolesgn2ores  27636  nogesgn1ores  27638  nosepdmlem  27647  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  axtg5seg  28533  axtgupdim2  28539  axtgeucl  28540  axlowdim1  29028  lpvtx  29137  umgrnloopv  29175  usgrnloopvALT  29270  umgrvad2edg  29282  cusgrfilem2  29525  pthdlem2lem  29835  iswwlks  29904  iswwlksnx  29908  2pthdlem1  29998  isclwwlk  30054  3pthdlem1  30234  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2lem2  30289  eupth2lem3lem4  30301  eupth2lem3lem6  30303  3cyclfrgrrn1  30355  4cycl2vnunb  30360  frgrreg  30464  norm1exi  31321  shintcl  31401  chintcl  31403  chne0  31565  elspansn2  31638  eigre  31906  eigorth  31909  kbpj  32027  superpos  32425  hatomic  32431  isprmidl  33498  ismxidl  33522  ssmxidllem  33533  ssmxidl  33534  constrconj  33889  constrcccllem  33898  constrcbvlem  33899  2sqr3minply  33924  zarcmplem  34025  xrge0iifhom  34081  xrge0iif1  34082  esumpr2  34211  sibfof  34484  signswn0  34704  signswch  34705  signstfvneq0  34716  axtgupdim2ALTV  34812  bnj168  34873  bnj970  35089  bnj1154  35141  onvf1odlem2  35286  umgracycusgr  35336  cusgracyclt3v  35338  subfacp1lem1  35361  erdszelem8  35380  indispconn  35416  cvmsss2  35456  nepss  35900  elwlim  36003  dfrdg4  36133  fvray  36323  linedegen  36325  fvline  36326  hilbert1.1  36336  rankeq1o  36353  unblimceq0lem  36766  knoppndvlem21  36792  qdiff  37641  poimirlem1  37942  poimirlem17  37958  poimirlem20  37961  poimirlem32  37973  itg2addnclem3  37994  neificl  38074  isdrngo3  38280  ispridl  38355  ismaxidl  38361  islshp  39425  lsatn0  39445  lshpset2N  39565  atlex  39762  hlsuprexch  39827  3dimlem1  39904  llni2  39958  lplni2  39983  2llnjN  40013  lvoli2  40027  2lplnj  40066  islinei  40186  lnatexN  40225  llnexchb2  40315  lhpmatb  40477  cdleme40m  40913  cdlemftr3  41011  cdlemk28-3  41354  cdlemk35s  41383  cdlemk39s  41385  cdlemk42  41387  nnn1suc  42704  dnnumch1  43472  aomclem3  43484  aomclem8  43489  dfac11  43490  dfacbasgrp  43536  dfsucon  43950  ax6e2ndeq  44986  ax6e2ndeqVD  45335  relpfrlem  45380  permac8prim  45441  fnchoice  45460  fiiuncl  45496  disjrnmpt2  45618  idlimc  46056  limcperiod  46058  limclner  46079  cnrefiisp  46258  climxlim2lem  46273  fperdvper  46347  stoweidlem35  46463  stoweidlem43  46471  stoweidlem59  46487  fourierdlem76  46610  etransclem47  46709  nnfoctbdjlem  46883  elprneb  47477  ichexmpl1  47929  ichnreuop  47932  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  usgrgrtrirex  48426  isubgr3stgrlem4  48445  usgrexmpl2trifr  48513  gpg3kgrtriex  48565  itcoval2  49140  itcoval3  49141  itcovalsuc  49143  ackvalsuc1mpt  49154  inlinecirc02plem  49262  oppcthinendcALT  49916