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 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  pm13.18  3013  pm13.181  3014  nelrdva  3663  psseq1  4042  n0snor2el  4789  0inp0  5304  nnullss  5410  opeqex  5446  frsn  5712  xp11  6133  limeq  6329  tz6.12i  6860  fveqressseq  7024  funopsn  7093  fprg  7100  tpres  7147  f1dom3el3dif  7215  f1ounsn  7218  f1prex  7230  isofrlem  7286  resf1extb  7876  f1oweALT  7916  frxp  8068  xpord2lem  8084  poxp2  8085  frxp2  8086  xpord2indlem  8089  xpord3lem  8091  frxp3  8093  xpord3inddlem  8096  suppimacnv  8116  elqsn0  8721  frfi  9185  fiint  9227  marypha1lem  9336  frmin  9661  eldju2ndl  9836  dfac8alem  9939  dfac8clem  9942  aceq3lem  10030  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  dfac5  10039  dfac2b  10041  dfac9  10047  kmlem1  10061  kmlem12  10072  kmlem14  10074  fin2i  10205  isfin2-2  10229  fin23lem21  10249  fin1a2lem10  10319  axcc2lem  10346  dominf  10355  ac5b  10388  zornn0g  10415  axdclem  10429  dominfac  10484  elwina  10597  elina  10598  iswun  10615  rankcf  10688  axrrecex  11074  elimne0  11122  1re  11132  recex  11769  xnn0nemnf  12485  uzn0  12768  qreccl  12882  xrnemnf  13031  xrnepnf  13032  xnn0n0n1ge2b  13046  fztpval  13502  expcl2lem  13996  hashnemnf  14267  hashneq0  14287  hashge2el2difr  14404  hashdmpropge2  14406  relexp1g  14949  ntrivcvgn0  15821  ntrivcvgmullem  15824  fprodntriv  15865  divalglem7  16326  divalg  16330  gcdcllem1  16426  gcdcllem3  16428  pcpre1  16770  pcqmul  16781  pcqcl  16784  prmgaplem3  16981  prmgaplem4  16982  xpsfrnel  17483  mreintcl  17514  isdrs  18224  isipodrs  18460  sgrp2rid2ex  18852  frgpuptinv  19700  isnzr2  20451  nrhmzr  20470  isdrngrd  20699  isdrngrdOLD  20701  psgnodpmr  21545  lindfrn  21776  dmatelnd  22440  dmatmul  22441  mdetdiaglem  22542  mdetunilem1  22556  fvmptnn04ifa  22794  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  fiinopn  22845  hausnei  23272  dfconn2  23363  2ndcdisj  23400  regr1lem2  23684  isfbas  23773  ioorinv  25533  ioorcl  25534  vitalilem2  25566  vitalilem3  25567  vitali  25570  itg1climres  25671  mbfi1fseqlem4  25675  dvferm1lem  25944  dvferm2lem  25946  isuc1p  26102  ismon1p  26104  ply1remlem  26126  plydivlem4  26260  aannenlem1  26292  aannenlem2  26293  lgsne0  27302  lgsqr  27318  nolesgn2ores  27640  nogesgn1ores  27642  nosepdmlem  27651  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  axtg5seg  28537  axtgupdim2  28543  axtgeucl  28544  axlowdim1  29032  lpvtx  29141  umgrnloopv  29179  usgrnloopvALT  29274  umgrvad2edg  29286  cusgrfilem2  29530  pthdlem2lem  29840  iswwlks  29909  iswwlksnx  29913  2pthdlem1  30003  isclwwlk  30059  3pthdlem1  30239  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupth2lem2  30294  eupth2lem3lem4  30306  eupth2lem3lem6  30308  3cyclfrgrrn1  30360  4cycl2vnunb  30365  frgrreg  30469  norm1exi  31325  shintcl  31405  chintcl  31407  chne0  31569  elspansn2  31642  eigre  31910  eigorth  31913  kbpj  32031  superpos  32429  hatomic  32435  isprmidl  33519  ismxidl  33543  ssmxidllem  33554  ssmxidl  33555  constrconj  33902  constrcccllem  33911  constrcbvlem  33912  2sqr3minply  33937  zarcmplem  34038  xrge0iifhom  34094  xrge0iif1  34095  esumpr2  34224  sibfof  34497  signswn0  34717  signswch  34718  signstfvneq0  34729  axtgupdim2ALTV  34825  bnj168  34886  bnj970  35103  bnj1154  35155  onvf1odlem2  35298  umgracycusgr  35348  cusgracyclt3v  35350  subfacp1lem1  35373  erdszelem8  35392  indispconn  35428  cvmsss2  35468  nepss  35912  elwlim  36015  dfrdg4  36145  fvray  36335  linedegen  36337  fvline  36338  hilbert1.1  36348  rankeq1o  36365  unblimceq0lem  36706  knoppndvlem21  36732  poimirlem1  37822  poimirlem17  37838  poimirlem20  37841  poimirlem32  37853  itg2addnclem3  37874  neificl  37954  isdrngo3  38160  ispridl  38235  ismaxidl  38241  islshp  39239  lsatn0  39259  lshpset2N  39379  atlex  39576  hlsuprexch  39641  3dimlem1  39718  llni2  39772  lplni2  39797  2llnjN  39827  lvoli2  39841  2lplnj  39880  islinei  40000  lnatexN  40039  llnexchb2  40129  lhpmatb  40291  cdleme40m  40727  cdlemftr3  40825  cdlemk28-3  41168  cdlemk35s  41197  cdlemk39s  41199  cdlemk42  41201  nnn1suc  42521  dnnumch1  43286  aomclem3  43298  aomclem8  43303  dfac11  43304  dfacbasgrp  43350  dfsucon  43764  ax6e2ndeq  44800  ax6e2ndeqVD  45149  relpfrlem  45194  permac8prim  45255  fnchoice  45274  fiiuncl  45310  disjrnmpt2  45432  idlimc  45872  limcperiod  45874  limclner  45895  cnrefiisp  46074  climxlim2lem  46089  fperdvper  46163  stoweidlem35  46279  stoweidlem43  46287  stoweidlem59  46303  fourierdlem76  46426  etransclem47  46525  nnfoctbdjlem  46699  elprneb  47275  ichexmpl1  47715  ichnreuop  47718  vopnbgrel  48100  dfclnbgr6  48102  dfnbgr6  48103  usgrgrtrirex  48196  isubgr3stgrlem4  48215  usgrexmpl2trifr  48283  gpg3kgrtriex  48335  itcoval2  48910  itcoval3  48911  itcovalsuc  48913  ackvalsuc1mpt  48924  inlinecirc02plem  49032  oppcthinendcALT  49686