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 1542   ≠ wne 2933

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 2709

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

This theorem is referenced by:  pm13.18  3014  pm13.181  3015  nelrdva  3652  psseq1  4031  n0snor2el  4777  0inp0  5294  nnullss  5407  opeqex  5444  frsn  5710  xp11  6131  limeq  6327  tz6.12i  6858  fveqressseq  7023  funopsn  7093  fprg  7100  tpres  7147  f1dom3el3dif  7215  f1ounsn  7218  f1prex  7230  isofrlem  7286  resf1extb  7876  f1oweALT  7916  frxp  8067  xpord2lem  8083  poxp2  8084  frxp2  8085  xpord2indlem  8088  xpord3lem  8090  frxp3  8092  xpord3inddlem  8095  suppimacnv  8115  elqsn0  8722  frfi  9186  fiint  9228  marypha1lem  9337  frmin  9662  eldju2ndl  9837  dfac8alem  9940  dfac8clem  9943  aceq3lem  10031  dfac5lem3  10036  dfac5lem4  10037  dfac5lem4OLD  10039  dfac5  10040  dfac2b  10042  dfac9  10048  kmlem1  10062  kmlem12  10073  kmlem14  10075  fin2i  10206  isfin2-2  10230  fin23lem21  10250  fin1a2lem10  10320  axcc2lem  10347  dominf  10356  ac5b  10389  zornn0g  10416  axdclem  10430  dominfac  10485  elwina  10598  elina  10599  iswun  10616  rankcf  10689  axrrecex  11075  elimne0  11123  1re  11133  recex  11771  xnn0nemnf  12510  uzn0  12794  qreccl  12908  xrnemnf  13057  xrnepnf  13058  xnn0n0n1ge2b  13072  fztpval  13529  expcl2lem  14024  hashnemnf  14295  hashneq0  14315  hashge2el2difr  14432  hashdmpropge2  14434  relexp1g  14977  ntrivcvgn0  15852  ntrivcvgmullem  15855  fprodntriv  15896  divalglem7  16357  divalg  16361  gcdcllem1  16457  gcdcllem3  16459  pcpre1  16802  pcqmul  16813  pcqcl  16816  prmgaplem3  17013  prmgaplem4  17014  xpsfrnel  17515  mreintcl  17546  isdrs  18256  isipodrs  18492  sgrp2rid2ex  18887  frgpuptinv  19735  isnzr2  20484  nrhmzr  20503  isdrngrd  20732  isdrngrdOLD  20734  psgnodpmr  21578  lindfrn  21809  dmatelnd  22470  dmatmul  22471  mdetdiaglem  22572  mdetunilem1  22586  fvmptnn04ifa  22824  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  fiinopn  22875  hausnei  23302  dfconn2  23393  2ndcdisj  23430  regr1lem2  23714  isfbas  23803  ioorinv  25552  ioorcl  25553  vitalilem2  25585  vitalilem3  25586  vitali  25589  itg1climres  25690  mbfi1fseqlem4  25694  dvferm1lem  25960  dvferm2lem  25962  isuc1p  26118  ismon1p  26120  ply1remlem  26142  plydivlem4  26275  aannenlem1  26307  aannenlem2  26308  lgsne0  27317  lgsqr  27333  nolesgn2ores  27655  nogesgn1ores  27657  nosepdmlem  27666  nosupbnd1lem3  27693  nosupbnd1lem5  27695  nosupbnd2lem1  27698  noinfbnd1lem3  27708  noinfbnd1lem5  27710  noinfbnd2lem1  27713  axtg5seg  28552  axtgupdim2  28558  axtgeucl  28559  axlowdim1  29047  lpvtx  29156  umgrnloopv  29194  usgrnloopvALT  29289  umgrvad2edg  29301  cusgrfilem2  29545  pthdlem2lem  29855  iswwlks  29924  iswwlksnx  29928  2pthdlem1  30018  isclwwlk  30074  3pthdlem1  30254  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  eupth2lem2  30309  eupth2lem3lem4  30321  eupth2lem3lem6  30323  3cyclfrgrrn1  30375  4cycl2vnunb  30380  frgrreg  30484  norm1exi  31341  shintcl  31421  chintcl  31423  chne0  31585  elspansn2  31658  eigre  31926  eigorth  31929  kbpj  32047  superpos  32445  hatomic  32451  isprmidl  33518  ismxidl  33542  ssmxidllem  33553  ssmxidl  33554  constrconj  33910  constrcccllem  33919  constrcbvlem  33920  2sqr3minply  33945  zarcmplem  34046  xrge0iifhom  34102  xrge0iif1  34103  esumpr2  34232  sibfof  34505  signswn0  34725  signswch  34726  signstfvneq0  34737  axtgupdim2ALTV  34833  bnj168  34894  bnj970  35110  bnj1154  35162  onvf1odlem2  35307  umgracycusgr  35357  cusgracyclt3v  35359  subfacp1lem1  35382  erdszelem8  35401  indispconn  35437  cvmsss2  35477  nepss  35921  elwlim  36024  dfrdg4  36154  fvray  36344  linedegen  36346  fvline  36347  hilbert1.1  36357  rankeq1o  36374  unblimceq0lem  36779  knoppndvlem21  36805  poimirlem1  37953  poimirlem17  37969  poimirlem20  37972  poimirlem32  37984  itg2addnclem3  38005  neificl  38085  isdrngo3  38291  ispridl  38366  ismaxidl  38372  islshp  39436  lsatn0  39456  lshpset2N  39576  atlex  39773  hlsuprexch  39838  3dimlem1  39915  llni2  39969  lplni2  39994  2llnjN  40024  lvoli2  40038  2lplnj  40077  islinei  40197  lnatexN  40236  llnexchb2  40326  lhpmatb  40488  cdleme40m  40924  cdlemftr3  41022  cdlemk28-3  41365  cdlemk35s  41394  cdlemk39s  41396  cdlemk42  41398  nnn1suc  42715  dnnumch1  43487  aomclem3  43499  aomclem8  43504  dfac11  43505  dfacbasgrp  43551  dfsucon  43965  ax6e2ndeq  45001  ax6e2ndeqVD  45350  relpfrlem  45395  permac8prim  45456  fnchoice  45475  fiiuncl  45511  disjrnmpt2  45633  idlimc  46071  limcperiod  46073  limclner  46094  cnrefiisp  46273  climxlim2lem  46288  fperdvper  46362  stoweidlem35  46478  stoweidlem43  46486  stoweidlem59  46502  fourierdlem76  46625  etransclem47  46724  nnfoctbdjlem  46898  elprneb  47474  ichexmpl1  47926  ichnreuop  47929  vopnbgrel  48327  dfclnbgr6  48329  dfnbgr6  48330  usgrgrtrirex  48423  isubgr3stgrlem4  48442  usgrexmpl2trifr  48510  gpg3kgrtriex  48562  itcoval2  49137  itcoval3  49138  itcovalsuc  49140  ackvalsuc1mpt  49151  inlinecirc02plem  49259  oppcthinendcALT  49913