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  5296  nnullss  5409  opeqex  5446  frsn  5712  xp11  6133  limeq  6329  tz6.12i  6860  fveqressseq  7025  funopsn  7095  fprg  7102  tpres  7149  f1dom3el3dif  7217  f1ounsn  7220  f1prex  7232  isofrlem  7288  resf1extb  7878  f1oweALT  7918  frxp  8069  xpord2lem  8085  poxp2  8086  frxp2  8087  xpord2indlem  8090  xpord3lem  8092  frxp3  8094  xpord3inddlem  8097  suppimacnv  8117  elqsn0  8724  frfi  9188  fiint  9230  marypha1lem  9339  frmin  9664  eldju2ndl  9839  dfac8alem  9942  dfac8clem  9945  aceq3lem  10033  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  dfac5  10042  dfac2b  10044  dfac9  10050  kmlem1  10064  kmlem12  10075  kmlem14  10077  fin2i  10208  isfin2-2  10232  fin23lem21  10252  fin1a2lem10  10322  axcc2lem  10349  dominf  10358  ac5b  10391  zornn0g  10418  axdclem  10432  dominfac  10487  elwina  10600  elina  10601  iswun  10618  rankcf  10691  axrrecex  11077  elimne0  11125  1re  11135  recex  11773  xnn0nemnf  12512  uzn0  12796  qreccl  12910  xrnemnf  13059  xrnepnf  13060  xnn0n0n1ge2b  13074  fztpval  13531  expcl2lem  14026  hashnemnf  14297  hashneq0  14317  hashge2el2difr  14434  hashdmpropge2  14436  relexp1g  14979  ntrivcvgn0  15854  ntrivcvgmullem  15857  fprodntriv  15898  divalglem7  16359  divalg  16363  gcdcllem1  16459  gcdcllem3  16461  pcpre1  16804  pcqmul  16815  pcqcl  16818  prmgaplem3  17015  prmgaplem4  17016  xpsfrnel  17517  mreintcl  17548  isdrs  18258  isipodrs  18494  sgrp2rid2ex  18889  frgpuptinv  19737  isnzr2  20486  nrhmzr  20505  isdrngrd  20734  isdrngrdOLD  20736  psgnodpmr  21580  lindfrn  21811  dmatelnd  22471  dmatmul  22472  mdetdiaglem  22573  mdetunilem1  22587  fvmptnn04ifa  22825  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  fiinopn  22876  hausnei  23303  dfconn2  23394  2ndcdisj  23431  regr1lem2  23715  isfbas  23804  ioorinv  25553  ioorcl  25554  vitalilem2  25586  vitalilem3  25587  vitali  25590  itg1climres  25691  mbfi1fseqlem4  25695  dvferm1lem  25961  dvferm2lem  25963  isuc1p  26116  ismon1p  26118  ply1remlem  26140  plydivlem4  26273  aannenlem1  26305  aannenlem2  26306  lgsne0  27312  lgsqr  27328  nolesgn2ores  27650  nogesgn1ores  27652  nosepdmlem  27661  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  axtg5seg  28547  axtgupdim2  28553  axtgeucl  28554  axlowdim1  29042  lpvtx  29151  umgrnloopv  29189  usgrnloopvALT  29284  umgrvad2edg  29296  cusgrfilem2  29540  pthdlem2lem  29850  iswwlks  29919  iswwlksnx  29923  2pthdlem1  30013  isclwwlk  30069  3pthdlem1  30249  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupth2lem2  30304  eupth2lem3lem4  30316  eupth2lem3lem6  30318  3cyclfrgrrn1  30370  4cycl2vnunb  30375  frgrreg  30479  norm1exi  31336  shintcl  31416  chintcl  31418  chne0  31580  elspansn2  31653  eigre  31921  eigorth  31924  kbpj  32042  superpos  32440  hatomic  32446  isprmidl  33513  ismxidl  33537  ssmxidllem  33548  ssmxidl  33549  constrconj  33905  constrcccllem  33914  constrcbvlem  33915  2sqr3minply  33940  zarcmplem  34041  xrge0iifhom  34097  xrge0iif1  34098  esumpr2  34227  sibfof  34500  signswn0  34720  signswch  34721  signstfvneq0  34732  axtgupdim2ALTV  34828  bnj168  34889  bnj970  35105  bnj1154  35157  onvf1odlem2  35302  umgracycusgr  35352  cusgracyclt3v  35354  subfacp1lem1  35377  erdszelem8  35396  indispconn  35432  cvmsss2  35472  nepss  35916  elwlim  36019  dfrdg4  36149  fvray  36339  linedegen  36341  fvline  36342  hilbert1.1  36352  rankeq1o  36369  unblimceq0lem  36782  knoppndvlem21  36808  poimirlem1  37956  poimirlem17  37972  poimirlem20  37975  poimirlem32  37987  itg2addnclem3  38008  neificl  38088  isdrngo3  38294  ispridl  38369  ismaxidl  38375  islshp  39439  lsatn0  39459  lshpset2N  39579  atlex  39776  hlsuprexch  39841  3dimlem1  39918  llni2  39972  lplni2  39997  2llnjN  40027  lvoli2  40041  2lplnj  40080  islinei  40200  lnatexN  40239  llnexchb2  40329  lhpmatb  40491  cdleme40m  40927  cdlemftr3  41025  cdlemk28-3  41368  cdlemk35s  41397  cdlemk39s  41399  cdlemk42  41401  nnn1suc  42718  dnnumch1  43490  aomclem3  43502  aomclem8  43507  dfac11  43508  dfacbasgrp  43554  dfsucon  43968  ax6e2ndeq  45004  ax6e2ndeqVD  45353  relpfrlem  45398  permac8prim  45459  fnchoice  45478  fiiuncl  45514  disjrnmpt2  45636  idlimc  46074  limcperiod  46076  limclner  46097  cnrefiisp  46276  climxlim2lem  46291  fperdvper  46365  stoweidlem35  46481  stoweidlem43  46489  stoweidlem59  46505  fourierdlem76  46628  etransclem47  46727  nnfoctbdjlem  46901  elprneb  47489  ichexmpl1  47941  ichnreuop  47944  vopnbgrel  48342  dfclnbgr6  48344  dfnbgr6  48345  usgrgrtrirex  48438  isubgr3stgrlem4  48457  usgrexmpl2trifr  48525  gpg3kgrtriex  48577  itcoval2  49152  itcoval3  49153  itcovalsuc  49155  ackvalsuc1mpt  49166  inlinecirc02plem  49274  oppcthinendcALT  49928