Theorem neeq1 2991

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 2705

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

This theorem is referenced by:  pm13.18  3010  pm13.181  3011  nelrdva  3660  psseq1  4039  n0snor2el  4786  0inp0  5301  nnullss  5407  opeqex  5443  frsn  5709  xp11  6129  limeq  6325  tz6.12i  6856  fveqressseq  7020  funopsn  7089  fprg  7096  tpres  7143  f1dom3el3dif  7211  f1ounsn  7214  f1prex  7226  isofrlem  7282  resf1extb  7872  f1oweALT  7912  frxp  8064  xpord2lem  8080  poxp2  8081  frxp2  8082  xpord2indlem  8085  xpord3lem  8087  frxp3  8089  xpord3inddlem  8092  suppimacnv  8112  elqsn0  8716  frfi  9178  fiint  9220  marypha1lem  9326  frmin  9651  eldju2ndl  9826  dfac8alem  9929  dfac8clem  9932  aceq3lem  10020  dfac5lem3  10025  dfac5lem4  10026  dfac5lem4OLD  10028  dfac5  10029  dfac2b  10031  dfac9  10037  kmlem1  10051  kmlem12  10062  kmlem14  10064  fin2i  10195  isfin2-2  10219  fin23lem21  10239  fin1a2lem10  10309  axcc2lem  10336  dominf  10345  ac5b  10378  zornn0g  10405  axdclem  10419  dominfac  10473  elwina  10586  elina  10587  iswun  10604  rankcf  10677  axrrecex  11063  elimne0  11111  1re  11121  recex  11758  xnn0nemnf  12474  uzn0  12757  qreccl  12871  xrnemnf  13020  xrnepnf  13021  xnn0n0n1ge2b  13035  fztpval  13490  expcl2lem  13984  hashnemnf  14255  hashneq0  14275  hashge2el2difr  14392  hashdmpropge2  14394  relexp1g  14937  ntrivcvgn0  15809  ntrivcvgmullem  15812  fprodntriv  15853  divalglem7  16314  divalg  16318  gcdcllem1  16414  gcdcllem3  16416  pcpre1  16758  pcqmul  16769  pcqcl  16772  prmgaplem3  16969  prmgaplem4  16970  xpsfrnel  17470  mreintcl  17501  isdrs  18211  isipodrs  18447  sgrp2rid2ex  18839  frgpuptinv  19687  isnzr2  20437  nrhmzr  20456  isdrngrd  20685  isdrngrdOLD  20687  psgnodpmr  21531  lindfrn  21762  dmatelnd  22414  dmatmul  22415  mdetdiaglem  22516  mdetunilem1  22530  fvmptnn04ifa  22768  chfacfscmulgsum  22778  chfacfpmmulgsum  22782  fiinopn  22819  hausnei  23246  dfconn2  23337  2ndcdisj  23374  regr1lem2  23658  isfbas  23747  ioorinv  25507  ioorcl  25508  vitalilem2  25540  vitalilem3  25541  vitali  25544  itg1climres  25645  mbfi1fseqlem4  25649  dvferm1lem  25918  dvferm2lem  25920  isuc1p  26076  ismon1p  26078  ply1remlem  26100  plydivlem4  26234  aannenlem1  26266  aannenlem2  26267  lgsne0  27276  lgsqr  27292  nolesgn2ores  27614  nogesgn1ores  27616  nosepdmlem  27625  nosupbnd1lem3  27652  nosupbnd1lem5  27654  nosupbnd2lem1  27657  noinfbnd1lem3  27667  noinfbnd1lem5  27669  noinfbnd2lem1  27672  axtg5seg  28446  axtgupdim2  28452  axtgeucl  28453  axlowdim1  28941  lpvtx  29050  umgrnloopv  29088  usgrnloopvALT  29183  umgrvad2edg  29195  cusgrfilem2  29439  pthdlem2lem  29749  iswwlks  29818  iswwlksnx  29822  2pthdlem1  29912  isclwwlk  29968  3pthdlem1  30148  upgr3v3e3cycl  30164  upgr4cycl4dv4e  30169  eupth2lem2  30203  eupth2lem3lem4  30215  eupth2lem3lem6  30217  3cyclfrgrrn1  30269  4cycl2vnunb  30274  frgrreg  30378  norm1exi  31234  shintcl  31314  chintcl  31316  chne0  31478  elspansn2  31551  eigre  31819  eigorth  31822  kbpj  31940  superpos  32338  hatomic  32344  isprmidl  33412  ismxidl  33436  ssmxidllem  33447  ssmxidl  33448  constrconj  33781  constrcccllem  33790  constrcbvlem  33791  2sqr3minply  33816  zarcmplem  33917  xrge0iifhom  33973  xrge0iif1  33974  esumpr2  34103  sibfof  34376  signswn0  34596  signswch  34597  signstfvneq0  34608  axtgupdim2ALTV  34704  bnj168  34765  bnj970  34982  bnj1154  35034  onvf1odlem2  35171  umgracycusgr  35221  cusgracyclt3v  35223  subfacp1lem1  35246  erdszelem8  35265  indispconn  35301  cvmsss2  35341  nepss  35785  elwlim  35888  dfrdg4  36018  fvray  36208  linedegen  36210  fvline  36211  hilbert1.1  36221  rankeq1o  36238  unblimceq0lem  36573  knoppndvlem21  36599  poimirlem1  37684  poimirlem17  37700  poimirlem20  37703  poimirlem32  37715  itg2addnclem3  37736  neificl  37816  isdrngo3  38022  ispridl  38097  ismaxidl  38103  islshp  39101  lsatn0  39121  lshpset2N  39241  atlex  39438  hlsuprexch  39503  3dimlem1  39580  llni2  39634  lplni2  39659  2llnjN  39689  lvoli2  39703  2lplnj  39742  islinei  39862  lnatexN  39901  llnexchb2  39991  lhpmatb  40153  cdleme40m  40589  cdlemftr3  40687  cdlemk28-3  41030  cdlemk35s  41059  cdlemk39s  41061  cdlemk42  41063  nnn1suc  42387  dnnumch1  43164  aomclem3  43176  aomclem8  43181  dfac11  43182  dfacbasgrp  43228  dfsucon  43643  ax6e2ndeq  44679  ax6e2ndeqVD  45028  relpfrlem  45073  permac8prim  45134  fnchoice  45153  fiiuncl  45189  disjrnmpt2  45312  idlimc  45753  limcperiod  45755  limclner  45776  cnrefiisp  45955  climxlim2lem  45970  fperdvper  46044  stoweidlem35  46160  stoweidlem43  46168  stoweidlem59  46184  fourierdlem76  46307  etransclem47  46406  nnfoctbdjlem  46580  elprneb  47156  ichexmpl1  47596  ichnreuop  47599  vopnbgrel  47981  dfclnbgr6  47983  dfnbgr6  47984  usgrgrtrirex  48077  isubgr3stgrlem4  48096  usgrexmpl2trifr  48164  gpg3kgrtriex  48216  itcoval2  48792  itcoval3  48793  itcovalsuc  48795  ackvalsuc1mpt  48806  inlinecirc02plem  48914  oppcthinendcALT  49569