Theorem neeq1 2990

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  pm13.18  3009  pm13.181  3010  nelrdva  3664  psseq1  4040  n0snor2el  4785  0inp0  5297  nnullss  5402  opeqex  5438  frsn  5704  xp11  6122  limeq  6318  tz6.12i  6848  fveqressseq  7012  funopsn  7081  fprg  7088  tpres  7135  f1dom3el3dif  7203  f1ounsn  7206  f1prex  7218  isofrlem  7274  resf1extb  7864  f1oweALT  7904  frxp  8056  xpord2lem  8072  poxp2  8073  frxp2  8074  xpord2indlem  8077  xpord3lem  8079  frxp3  8081  xpord3inddlem  8084  suppimacnv  8104  elqsn0  8708  frfi  9169  fiint  9211  marypha1lem  9317  frmin  9642  eldju2ndl  9817  dfac8alem  9920  dfac8clem  9923  aceq3lem  10011  dfac5lem3  10016  dfac5lem4  10017  dfac5lem4OLD  10019  dfac5  10020  dfac2b  10022  dfac9  10028  kmlem1  10042  kmlem12  10053  kmlem14  10055  fin2i  10186  isfin2-2  10210  fin23lem21  10230  fin1a2lem10  10300  axcc2lem  10327  dominf  10336  ac5b  10369  zornn0g  10396  axdclem  10410  dominfac  10464  elwina  10577  elina  10578  iswun  10595  rankcf  10668  axrrecex  11054  elimne0  11102  1re  11112  recex  11749  xnn0nemnf  12465  uzn0  12749  qreccl  12867  xrnemnf  13016  xrnepnf  13017  xnn0n0n1ge2b  13031  fztpval  13486  expcl2lem  13980  hashnemnf  14251  hashneq0  14271  hashge2el2difr  14388  hashdmpropge2  14390  relexp1g  14933  ntrivcvgn0  15805  ntrivcvgmullem  15808  fprodntriv  15849  divalglem7  16310  divalg  16314  gcdcllem1  16410  gcdcllem3  16412  pcpre1  16754  pcqmul  16765  pcqcl  16768  prmgaplem3  16965  prmgaplem4  16966  xpsfrnel  17466  mreintcl  17497  isdrs  18207  isipodrs  18443  sgrp2rid2ex  18835  frgpuptinv  19684  isnzr2  20434  nrhmzr  20453  isdrngrd  20682  isdrngrdOLD  20684  psgnodpmr  21528  lindfrn  21759  dmatelnd  22412  dmatmul  22413  mdetdiaglem  22514  mdetunilem1  22528  fvmptnn04ifa  22766  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  fiinopn  22817  hausnei  23244  dfconn2  23335  2ndcdisj  23372  regr1lem2  23656  isfbas  23745  ioorinv  25505  ioorcl  25506  vitalilem2  25538  vitalilem3  25539  vitali  25542  itg1climres  25643  mbfi1fseqlem4  25647  dvferm1lem  25916  dvferm2lem  25918  isuc1p  26074  ismon1p  26076  ply1remlem  26098  plydivlem4  26232  aannenlem1  26264  aannenlem2  26265  lgsne0  27274  lgsqr  27290  nolesgn2ores  27612  nogesgn1ores  27614  nosepdmlem  27623  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd2lem1  27655  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd2lem1  27670  axtg5seg  28444  axtgupdim2  28450  axtgeucl  28451  axlowdim1  28938  lpvtx  29047  umgrnloopv  29085  usgrnloopvALT  29180  umgrvad2edg  29192  cusgrfilem2  29436  pthdlem2lem  29746  iswwlks  29815  iswwlksnx  29819  2pthdlem1  29909  isclwwlk  29962  3pthdlem1  30142  upgr3v3e3cycl  30158  upgr4cycl4dv4e  30163  eupth2lem2  30197  eupth2lem3lem4  30209  eupth2lem3lem6  30211  3cyclfrgrrn1  30263  4cycl2vnunb  30268  frgrreg  30372  norm1exi  31228  shintcl  31308  chintcl  31310  chne0  31472  elspansn2  31545  eigre  31813  eigorth  31816  kbpj  31934  superpos  32332  hatomic  32338  isprmidl  33401  ismxidl  33425  ssmxidllem  33436  ssmxidl  33437  constrconj  33756  constrcccllem  33765  constrcbvlem  33766  2sqr3minply  33791  zarcmplem  33892  xrge0iifhom  33948  xrge0iif1  33949  esumpr2  34078  sibfof  34351  signswn0  34571  signswch  34572  signstfvneq0  34583  axtgupdim2ALTV  34679  bnj168  34740  bnj970  34957  bnj1154  35009  onvf1odlem2  35146  umgracycusgr  35196  cusgracyclt3v  35198  subfacp1lem1  35221  erdszelem8  35240  indispconn  35276  cvmsss2  35316  nepss  35760  elwlim  35863  dfrdg4  35991  fvray  36181  linedegen  36183  fvline  36184  hilbert1.1  36194  rankeq1o  36211  unblimceq0lem  36546  knoppndvlem21  36572  poimirlem1  37667  poimirlem17  37683  poimirlem20  37686  poimirlem32  37698  itg2addnclem3  37719  neificl  37799  isdrngo3  38005  ispridl  38080  ismaxidl  38086  islshp  39024  lsatn0  39044  lshpset2N  39164  atlex  39361  hlsuprexch  39426  3dimlem1  39503  llni2  39557  lplni2  39582  2llnjN  39612  lvoli2  39626  2lplnj  39665  islinei  39785  lnatexN  39824  llnexchb2  39914  lhpmatb  40076  cdleme40m  40512  cdlemftr3  40610  cdlemk28-3  40953  cdlemk35s  40982  cdlemk39s  40984  cdlemk42  40986  nnn1suc  42305  dnnumch1  43083  aomclem3  43095  aomclem8  43100  dfac11  43101  dfacbasgrp  43147  dfsucon  43562  ax6e2ndeq  44598  ax6e2ndeqVD  44947  relpfrlem  44992  permac8prim  45053  fnchoice  45072  fiiuncl  45108  disjrnmpt2  45231  idlimc  45672  limcperiod  45674  limclner  45695  cnrefiisp  45874  climxlim2lem  45889  fperdvper  45963  stoweidlem35  46079  stoweidlem43  46087  stoweidlem59  46103  fourierdlem76  46226  etransclem47  46325  nnfoctbdjlem  46499  elprneb  47066  ichexmpl1  47506  ichnreuop  47509  vopnbgrel  47891  dfclnbgr6  47893  dfnbgr6  47894  usgrgrtrirex  47987  isubgr3stgrlem4  48006  usgrexmpl2trifr  48074  gpg3kgrtriex  48126  itcoval2  48702  itcoval3  48703  itcovalsuc  48705  ackvalsuc1mpt  48716  inlinecirc02plem  48824  oppcthinendcALT  49479