Theorem neeq1 3049

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  pm13.18  3068  nelrdva  3644  psseq1  4015  n0snor2el  4724  0inp0  5224  nnullss  5319  opeqex  5353  fri  5481  frsn  5603  xp11  5999  limeq  6171  tz6.12i  6671  fveqressseq  6824  funopsn  6887  fprg  6894  tpres  6940  f1dom3el3dif  7005  f1prex  7018  isofrlem  7072  f1oweALT  7655  frxp  7803  suppimacnv  7824  elqsn0  8349  frfi  8747  fiint  8779  marypha1lem  8881  eldju2ndl  9337  dfac8alem  9440  dfac8clem  9443  aceq3lem  9531  dfac5lem3  9536  dfac5lem4  9537  dfac5  9539  dfac2b  9541  dfac9  9547  kmlem1  9561  kmlem12  9572  kmlem14  9574  fin2i  9706  isfin2-2  9730  fin23lem21  9750  fin1a2lem10  9820  axcc2lem  9847  dominf  9856  ac5b  9889  zornn0g  9916  axdclem  9930  dominfac  9984  elwina  10097  elina  10098  iswun  10115  rankcf  10188  axrrecex  10574  elimne0  10620  1re  10630  recex  11261  xnn0nemnf  11966  uzn0  12248  qreccl  12356  xrnemnf  12500  xrnepnf  12501  xnn0n0n1ge2b  12514  fztpval  12964  expcl2lem  13437  hashnemnf  13700  hashneq0  13721  hashge2el2difr  13835  hashdmpropge2  13837  relexp1g  14377  ntrivcvgn0  15246  ntrivcvgmullem  15249  fprodntriv  15288  divalglem7  15740  divalg  15744  gcdcllem1  15838  gcdcllem3  15840  pcpre1  16169  pcqmul  16180  pcqcl  16183  prmgaplem3  16379  prmgaplem4  16380  xpsfrnel  16827  mreintcl  16858  isdrs  17536  isipodrs  17763  sgrp2rid2ex  18084  frgpuptinv  18889  isdrngrd  19521  isnzr2  20029  psgnodpmr  20279  lindfrn  20510  dmatelnd  21101  dmatmul  21102  mdetdiaglem  21203  mdetunilem1  21217  fvmptnn04ifa  21455  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  fiinopn  21506  hausnei  21933  dfconn2  22024  2ndcdisj  22061  regr1lem2  22345  isfbas  22434  ioorinv  24180  ioorcl  24181  vitalilem2  24213  vitalilem3  24214  vitali  24217  itg1climres  24318  mbfi1fseqlem4  24322  dvferm1lem  24587  dvferm2lem  24589  isuc1p  24741  ismon1p  24743  ply1remlem  24763  plydivlem4  24892  aannenlem1  24924  aannenlem2  24925  lgsne0  25919  lgsqr  25935  axtg5seg  26259  axtgupdim2  26265  axtgeucl  26266  axlowdim1  26753  lpvtx  26861  umgrnloopv  26899  usgrnloopvALT  26991  umgrvad2edg  27003  cusgrfilem2  27246  pthdlem2lem  27556  iswwlks  27622  iswwlksnx  27626  2pthdlem1  27716  isclwwlk  27769  3pthdlem1  27949  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eupth2lem2  28004  eupth2lem3lem4  28016  eupth2lem3lem6  28018  3cyclfrgrrn1  28070  4cycl2vnunb  28075  frgrreg  28179  norm1exi  29033  shintcl  29113  chintcl  29115  chne0  29277  elspansn2  29350  eigre  29618  eigorth  29621  kbpj  29739  superpos  30137  hatomic  30143  isprmidl  31021  ismxidl  31042  ssmxidllem  31049  ssmxidl  31050  zarcmplem  31234  xrge0iifhom  31290  xrge0iif1  31291  esumpr2  31436  sibfof  31708  signswn0  31940  signswch  31941  signstfvneq0  31952  axtgupdim2ALTV  32049  bnj168  32110  bnj970  32329  bnj1154  32381  umgracycusgr  32514  cusgracyclt3v  32516  subfacp1lem1  32539  erdszelem8  32558  indispconn  32594  cvmsss2  32634  nepss  33061  frmin  33197  elwlim  33223  nolesgn2ores  33292  nosepdmlem  33300  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd2lem1  33328  dfrdg4  33525  fvray  33715  linedegen  33717  fvline  33718  hilbert1.1  33728  rankeq1o  33745  unblimceq0lem  33958  knoppndvlem21  33984  poimirlem1  35058  poimirlem17  35074  poimirlem20  35077  poimirlem32  35089  itg2addnclem3  35110  neificl  35191  isdrngo3  35397  ispridl  35472  ismaxidl  35478  islshp  36275  lsatn0  36295  lshpset2N  36415  atlex  36612  hlsuprexch  36677  3dimlem1  36754  llni2  36808  lplni2  36833  2llnjN  36863  lvoli2  36877  2lplnj  36916  islinei  37036  lnatexN  37075  llnexchb2  37165  lhpmatb  37327  cdleme40m  37763  cdlemftr3  37861  cdlemk28-3  38204  cdlemk35s  38233  cdlemk39s  38235  cdlemk42  38237  metakunt30  39379  nnn1suc  39467  dnnumch1  39988  aomclem3  40000  aomclem8  40005  dfac11  40006  dfacbasgrp  40052  dfsucon  40231  ax6e2ndeq  41265  ax6e2ndeqVD  41615  fnchoice  41658  fiiuncl  41699  disjrnmpt2  41815  idlimc  42268  limcperiod  42270  limclner  42293  cnrefiisp  42472  climxlim2lem  42487  fperdvper  42561  stoweidlem35  42677  stoweidlem43  42685  stoweidlem59  42701  fourierdlem76  42824  etransclem47  42923  nnfoctbdjlem  43094  elprneb  43621  ichexmpl1  43986  ichnreuop  43989  nrhmzr  44497  itcoval2  45078  itcoval3  45079  itcovalsuc  45081  ackvalsuc1mpt  45092  inlinecirc02plem  45200