Theorem neeq1 3018

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  pm13.18  3037  pm13.181  3038  nelrdva  3666  psseq1  4041  n0snor2el  4788  0inp0  5312  nnullss  5426  opeqex  5464  frsn  5731  xp11  6155  limeq  6352  tz6.12i  6887  fveqressseq  7054  funopsnOLD  7125  fprg  7132  tpres  7179  f1dom3el3dif  7247  f1ounsn  7250  f1prex  7262  isofrlem  7318  resf1extb  7909  f1oweALT  7947  frxp  8099  xpord2lem  8115  poxp2  8116  frxp2  8117  xpord2indlem  8120  xpord3lem  8122  frxp3  8124  xpord3inddlem  8127  suppimacnv  8147  elqsn0  8759  frfi  9222  fiint  9264  marypha1lem  9372  frmin  9700  eldju2ndl  9875  dfac8alem  9978  dfac8clem  9981  aceq3lem  10069  dfac5lem3  10074  dfac5lem4  10075  dfac5lem4OLD  10077  dfac5  10078  dfac2b  10080  dfac9  10086  kmlem1  10100  kmlem12  10111  kmlem14  10113  fin2i  10245  isfin2-2  10269  fin23lem21  10289  fin1a2lem10  10359  axcc2lem  10386  dominf  10395  ac5b  10428  zornn0g  10455  axdclem  10469  dominfac  10524  elwina  10637  elina  10638  iswun  10655  rankcf  10728  axrrecex  11114  elimne0  11162  1re  11174  recex  11812  xnn0nemnf  12558  uzn0  12849  qreccl  12963  xrnemnf  13112  xrnepnf  13113  xnn0n0n1ge2b  13127  fztpval  13584  expcl2lem  14079  hashnemnf  14350  hashneq0  14370  hashge2el2difr  14487  hashdmpropge2  14489  relexp1g  15032  ntrivcvgn0  15918  ntrivcvgmullem  15921  fprodntriv  15962  divalglem7  16423  divalg  16427  gcdcllem1  16523  gcdcllem3  16525  pcpre1  16868  pcqmul  16879  pcqcl  16882  prmgaplem3  17079  prmgaplem4  17080  xpsfrnel  17582  mreintcl  17613  isdrs  18323  isipodrs  18559  sgrp2rid2ex  18954  frgpuptinv  19801  isnzr2  20554  nrhmzr  20573  isdrngrd  20802  isdrngrdOLD  20804  psgnodpmr  21629  lindfrn  21860  dmatelnd  22543  dmatmul  22544  mdetdiaglem  22645  mdetunilem1  22659  fvmptnn04ifa  22897  chfacfscmulgsum  22907  chfacfpmmulgsum  22911  fiinopn  22948  hausnei  23375  dfconn2  23466  2ndcdisj  23503  regr1lem2  23787  isfbas  23876  ioorinv  25625  ioorcl  25626  vitalilem2  25658  vitalilem3  25659  vitali  25662  itg1climres  25763  mbfi1fseqlem4  25767  dvferm1lem  26033  dvferm2lem  26035  isuc1p  26188  ismon1p  26190  ply1remlem  26212  plydivlem4  26347  aannenlem1  26379  aannenlem2  26380  lgsne0  27386  lgsqr  27402  nolesgn2ores  27723  nogesgn1ores  27725  nosepdmlem  27734  nosupbnd1lem3  27761  nosupbnd1lem5  27763  nosupbnd2lem1  27766  noinfbnd1lem3  27776  noinfbnd1lem5  27778  noinfbnd2lem1  27781  axtg5seg  28621  axtgupdim2  28627  axtgeucl  28628  axlowdim1  29116  lpvtx  29225  umgrnloopv  29263  usgrnloopvALT  29358  umgrvad2edg  29370  cusgrfilem2  29613  pthdlem2lem  29923  iswwlks  29992  iswwlksnx  29996  2pthdlem1  30086  isclwwlk  30142  3pthdlem1  30322  upgr3v3e3cycl  30338  upgr4cycl4dv4e  30343  eupth2lem2  30377  eupth2lem3lem4  30389  eupth2lem3lem6  30391  3cyclfrgrrn1  30443  4cycl2vnunb  30448  frgrreg  30552  norm1exi  31409  shintcl  31489  chintcl  31491  chne0  31653  elspansn2  31726  eigre  31994  eigorth  31997  kbpj  32115  superpos  32513  hatomic  32519  isprmidl  33584  ismxidl  33610  ssmxidllem  33621  ssmxidl  33622  constrconj  34002  constrcccllem  34011  constrcbvlem  34012  2sqr3minply  34037  zarcmplem  34138  xrge0iifhom  34194  xrge0iif1  34195  esumpr2  34324  sibfof  34597  signswn0  34814  signswch  34815  signstfvneq0  34826  axtgupdim2ALTV  34922  bnj168  34986  bnj970  35202  bnj1154  35254  onvf1odlem2  35407  umgracycusgr  35464  cusgracyclt3v  35466  subfacp1lem1  35489  erdszelem8  35508  indispconn  35544  cvmsss2  35584  nepss  36028  elwlim  36131  dfrdg4  36261  fvray  36451  linedegen  36453  fvline  36454  hilbert1.1  36464  rankeq1o  36481  unblimceq0lem  36904  knoppndvlem21  36930  qdiff  37779  poimirlem1  38080  poimirlem17  38096  poimirlem20  38099  poimirlem32  38111  itg2addnclem3  38132  neificl  38212  isdrngo3  38418  ispridl  38493  ismaxidl  38499  islshp  39563  lsatn0  39583  lshpset2N  39703  atlex  39900  hlsuprexch  39965  3dimlem1  40042  llni2  40096  lplni2  40121  2llnjN  40151  lvoli2  40165  2lplnj  40204  islinei  40324  lnatexN  40363  llnexchb2  40453  lhpmatb  40615  cdleme40m  41051  cdlemftr3  41149  cdlemk28-3  41492  cdlemk35s  41521  cdlemk39s  41523  cdlemk42  41525  nnn1suc  42841  dnnumch1  43581  aomclem3  43593  aomclem8  43598  dfac11  43599  dfacbasgrp  43645  dfsucon  44059  ax6e2ndeq  45095  ax6e2ndeqVD  45444  relpfrlem  45489  permac8prim  45550  fnchoice  45569  fiiuncl  45605  disjrnmpt2  45726  idlimc  46162  limcperiod  46164  limclner  46185  cnrefiisp  46364  climxlim2lem  46379  fperdvper  46453  stoweidlem35  46569  stoweidlem43  46577  stoweidlem59  46593  fourierdlem76  46716  etransclem47  46815  nnfoctbdjlem  46989  elprneb  47583  ichexmpl1  48035  ichnreuop  48038  vopnbgrel  48436  dfclnbgr6  48438  dfnbgr6  48439  usgrgrtrirex  48532  isubgr3stgrlem4  48551  usgrexmpl2trifr  48619  gpg3kgrtriex  48671  itcoval2  49246  itcoval3  49247  itcovalsuc  49249  ackvalsuc1mpt  49260  inlinecirc02plem  49368  oppcthinendcALT  50022