Theorem eqtr2i 2803

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)

Hypotheses

Ref	Expression
eqtr2i.1	⊢ 𝐴 = 𝐵
eqtr2i.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtr2i	⊢ 𝐶 = 𝐴

Proof of Theorem eqtr2i

Step	Hyp	Ref	Expression
1		eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2i.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtri 2802	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2787	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  3eqtrri  2807  3eqtr2ri  2809  dfun3  4092  dfif3  4321  dfsn2  4411  prprc1  4532  diftpsn3  4564  ssunpr  4594  sstp  4596  unidif0  5072  pwundif  5258  xpindi  5501  xpindir  5502  dmcnvcnv  5593  rncnvcnv  5594  imainrect  5829  dfrn4  5849  fcoi1  6328  foimacnv  6408  f1ossf1o  6660  fsnunfv  6724  difex2  7246  dfoprab3  7503  offval22  7534  fvmpt2curryd  7679  mapsnconst  8189  sbthlem8  8365  fiint  8525  ordtypecbv  8711  ruv  8796  trcl  8901  rankxplim2  9040  infcda1  9350  cfval2  9417  itunitc  9578  ituniiun  9579  hsmex2  9590  ltexnq  10132  ixi  11004  zeo  11815  num0h  11857  dec10p  11889  fseq1p1m1  12732  cats1fvn  14009  s3fn  14062  fsumrelem  14943  ef0lem  15211  ef01bndlem  15316  sadcadd  15586  sadadd2  15588  3lcm2e6woprm  15734  mod2xnegi  16179  decexp2  16183  str0  16307  ressinbas  16332  mreexexlem4d  16693  0g0  17649  frmdplusg  17778  sgrp2nmndlem4  17802  sgrp2nmndlem5  17803  oppgplusfval  18161  psgnsn  18324  psgnprfval1  18326  frgpnabllem1  18662  opprmulfval  19012  opprringb  19019  opprunit  19048  00lsp  19376  psrmulr  19781  ltbwe  19869  ply1plusgfvi  20008  chrval  20269  dsmmelbas  20482  mat2pmatfval  20935  unisngl  21739  qtopres  21910  ufildr  22143  oppgtmd  22309  tgioo  23007  tgqioo  23011  dveflem  24179  lhop1lem  24213  sincos4thpi  24703  coskpi  24710  cxpsqrtlem  24885  log2ublem1  25125  efrlim  25148  basellem3  25261  bposlem9  25469  graop  26377  0grsubgr  26625  usgrfilem  26674  finsumvtxdg2ssteplem4  26896  wlkvtxedg  26991  2wlkdlem1  27305  2pthd  27320  wlk2v2e  27560  3wlkdlem1  27562  3pthd  27577  konigsberg  27663  cnidOLD  28009  ip1ilem  28253  ipasslem10  28266  normlem6  28544  dfhnorm2  28551  h1de2i  28984  spansnji  29077  pjneli  29154  mayetes3i  29160  pjclem1  29626  mdslmd3i  29763  atabsi  29832  imadifxp  29977  dfdec100  30140  dpmul100  30167  dpmul1000  30169  dpmul4  30184  xrge00  30248  locfinref  30506  cnvordtrestixx  30557  raddcn  30573  rrhcn  30639  qqtopn  30653  esumpfinvallem  30734  isrnsigaOLD  30773  sxbrsigalem1  30945  eulerpartgbij  31032  sgnneg  31201  hgt750lem2  31332  subfacp1lem1  31760  subfacval2  31768  quad3  32161  ptrest  34034  poimirlem3  34038  poimirlem8  34043  poimirlem15  34050  mblfinlem3  34074  ismblfin  34076  areacirc  34130  pmapglb  35924  dvh4dimN  37601  hdmapfval  37981  sqdeccom12  38155  mapfzcons1  38240  lmhmlnmsplit  38616  pwssplit4  38618  clcnvlem  38887  cnvrcl0  38889  iunrelexp0  38951  sumnnodd  40770  climinf2mpt  40854  climinfmpt  40855  dvnmul  41086  wallispilem4  41212  dirkertrigeqlem3  41244  fourierdlem24  41275  fourierdlem57  41307  fourierdlem58  41308  fourierdlem80  41330  fourierswlem  41374  fouriersw  41375  fouriercn  41376  subsaliuncl  41500  gsumge0cl  41512  sge0tsms  41521  caragenuncllem  41653  0ome  41670  hoidmvle  41741  ovolval3  41788  ovolval4lem1  41790  smfpimbor1lem2  41933  gbpart7  42680  gbpart9  42682  gbpart11  42683  nnsum3primes4  42701  xpiun  42781  lindslinindsimp2lem5  43266  aacllem  43653