Theorem neeq1 3009

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  pm13.18  3028  pm13.181  3029  nelrdva  3727  psseq1  4113  n0snor2el  4858  0inp0  5377  nnullss  5482  opeqex  5517  friOLD  5658  frsn  5787  xp11  6206  limeq  6407  tz6.12i  6948  fveqressseq  7113  funopsn  7182  fprg  7189  tpres  7238  f1dom3el3dif  7306  f1prex  7320  isofrlem  7376  f1oweALT  8013  frxp  8167  xpord2lem  8183  poxp2  8184  frxp2  8185  xpord2indlem  8188  xpord3lem  8190  frxp3  8192  xpord3inddlem  8195  suppimacnv  8215  elqsn0  8844  frfi  9349  fiint  9394  fiintOLD  9395  marypha1lem  9502  frmin  9818  eldju2ndl  9993  dfac8alem  10098  dfac8clem  10101  aceq3lem  10189  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  dfac5  10198  dfac2b  10200  dfac9  10206  kmlem1  10220  kmlem12  10231  kmlem14  10233  fin2i  10364  isfin2-2  10388  fin23lem21  10408  fin1a2lem10  10478  axcc2lem  10505  dominf  10514  ac5b  10547  zornn0g  10574  axdclem  10588  dominfac  10642  elwina  10755  elina  10756  iswun  10773  rankcf  10846  axrrecex  11232  elimne0  11280  1re  11290  recex  11922  xnn0nemnf  12636  uzn0  12920  qreccl  13034  xrnemnf  13180  xrnepnf  13181  xnn0n0n1ge2b  13194  fztpval  13646  expcl2lem  14124  hashnemnf  14393  hashneq0  14413  hashge2el2difr  14530  hashdmpropge2  14532  relexp1g  15075  ntrivcvgn0  15946  ntrivcvgmullem  15949  fprodntriv  15990  divalglem7  16447  divalg  16451  gcdcllem1  16545  gcdcllem3  16547  pcpre1  16889  pcqmul  16900  pcqcl  16903  prmgaplem3  17100  prmgaplem4  17101  xpsfrnel  17622  mreintcl  17653  isdrs  18371  isipodrs  18607  sgrp2rid2ex  18962  frgpuptinv  19813  isnzr2  20544  nrhmzr  20563  isdrngrd  20788  isdrngrdOLD  20790  psgnodpmr  21631  lindfrn  21864  dmatelnd  22523  dmatmul  22524  mdetdiaglem  22625  mdetunilem1  22639  fvmptnn04ifa  22877  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  fiinopn  22928  hausnei  23357  dfconn2  23448  2ndcdisj  23485  regr1lem2  23769  isfbas  23858  ioorinv  25630  ioorcl  25631  vitalilem2  25663  vitalilem3  25664  vitali  25667  itg1climres  25769  mbfi1fseqlem4  25773  dvferm1lem  26042  dvferm2lem  26044  isuc1p  26200  ismon1p  26202  ply1remlem  26224  plydivlem4  26356  aannenlem1  26388  aannenlem2  26389  lgsne0  27397  lgsqr  27413  nolesgn2ores  27735  nogesgn1ores  27737  nosepdmlem  27746  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  axtg5seg  28491  axtgupdim2  28497  axtgeucl  28498  axlowdim1  28992  lpvtx  29103  umgrnloopv  29141  usgrnloopvALT  29236  umgrvad2edg  29248  cusgrfilem2  29492  pthdlem2lem  29803  iswwlks  29869  iswwlksnx  29873  2pthdlem1  29963  isclwwlk  30016  3pthdlem1  30196  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2lem2  30251  eupth2lem3lem4  30263  eupth2lem3lem6  30265  3cyclfrgrrn1  30317  4cycl2vnunb  30322  frgrreg  30426  norm1exi  31282  shintcl  31362  chintcl  31364  chne0  31526  elspansn2  31599  eigre  31867  eigorth  31870  kbpj  31988  superpos  32386  hatomic  32392  isprmidl  33431  ismxidl  33455  ssmxidllem  33466  ssmxidl  33467  constrconj  33735  2sqr3minply  33738  zarcmplem  33827  xrge0iifhom  33883  xrge0iif1  33884  esumpr2  34031  sibfof  34305  signswn0  34537  signswch  34538  signstfvneq0  34549  axtgupdim2ALTV  34645  bnj168  34706  bnj970  34923  bnj1154  34975  umgracycusgr  35122  cusgracyclt3v  35124  subfacp1lem1  35147  erdszelem8  35166  indispconn  35202  cvmsss2  35242  nepss  35680  elwlim  35787  dfrdg4  35915  fvray  36105  linedegen  36107  fvline  36108  hilbert1.1  36118  rankeq1o  36135  unblimceq0lem  36472  knoppndvlem21  36498  poimirlem1  37581  poimirlem17  37597  poimirlem20  37600  poimirlem32  37612  itg2addnclem3  37633  neificl  37713  isdrngo3  37919  ispridl  37994  ismaxidl  38000  islshp  38935  lsatn0  38955  lshpset2N  39075  atlex  39272  hlsuprexch  39338  3dimlem1  39415  llni2  39469  lplni2  39494  2llnjN  39524  lvoli2  39538  2lplnj  39577  islinei  39697  lnatexN  39736  llnexchb2  39826  lhpmatb  39988  cdleme40m  40424  cdlemftr3  40522  cdlemk28-3  40865  cdlemk35s  40894  cdlemk39s  40896  cdlemk42  40898  metakunt30  42191  nnn1suc  42255  dnnumch1  43001  aomclem3  43013  aomclem8  43018  dfac11  43019  dfacbasgrp  43065  dfsucon  43485  ax6e2ndeq  44530  ax6e2ndeqVD  44880  fnchoice  44929  fiiuncl  44967  disjrnmpt2  45095  idlimc  45547  limcperiod  45549  limclner  45572  cnrefiisp  45751  climxlim2lem  45766  fperdvper  45840  stoweidlem35  45956  stoweidlem43  45964  stoweidlem59  45980  fourierdlem76  46103  etransclem47  46202  nnfoctbdjlem  46376  elprneb  46944  ichexmpl1  47343  ichnreuop  47346  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  usgrgrtrirex  47799  usgrexmpl2trifr  47852  itcoval2  48398  itcoval3  48399  itcovalsuc  48401  ackvalsuc1mpt  48412  inlinecirc02plem  48520