Theorem eqtr2i 2762

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 2761	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2742	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  3eqtrri  2766  3eqtr2ri  2768  dfun3  4266  dfif3  4543  dfsn2  4642  prprc1  4770  diftpsn3  4806  ssunpr  4836  sstp  4838  unidif0  5359  xpindi  5834  xpindir  5835  dmcnvcnv  5933  rncnvcnv  5934  imainrect  6181  dfrn4  6202  predres  6341  fcoi1  6766  foimacnv  6851  f1ossf1o  7126  fsnunfv  7185  difex2  7747  dfoprab3  8040  offval22  8074  suppvalbr  8150  fvmpocurryd  8256  mapsnconst  8886  sbthlem8  9090  fiint  9324  ordtypecbv  9512  trcl  9723  rankxplim2  9875  infdju1  10184  cfval2  10255  itunitc  10416  ituniiun  10417  hsmex2  10428  ltexnq  10970  ixi  11843  zeo  12648  num0h  12689  dec10p  12720  fseq1p1m1  13575  cats1fvn  14809  s3fn  14862  fsumrelem  15753  ef0lem  16022  ef01bndlem  16127  sadcadd  16399  sadadd2  16401  3lcm2e6woprm  16552  mod2xnegi  17004  decexp2  17008  str0  17122  ressinbas  17190  mreexexlem4d  17591  0g0  18583  frmdplusg  18735  smndex1bas  18787  sgrp2nmndlem4  18809  sgrp2nmndlem5  18810  oppgplusfval  19212  symgsubmefmnd  19266  psgnsn  19388  psgnprfval1  19390  frgpnabllem1  19741  opprmulfval  20152  opprringb  20162  opprunit  20191  00lsp  20592  chrval  21077  dsmmelbas  21294  ltbwe  21599  ply1plusgfvi  21764  mat2pmatfval  22225  unisngl  23031  qtopres  23202  ufildr  23435  oppgtmd  23601  tgioo  24312  tgqioo  24316  dveflem  25496  lhop1lem  25530  sincos4thpi  26023  coskpi  26032  cxpsqrtlem  26210  log2ublem1  26451  efrlim  26474  basellem3  26587  bposlem9  26795  madeun  27379  precsexlem11  27666  graop  28320  0grsubgr  28566  usgrfilem  28615  finsumvtxdg2ssteplem4  28836  wlkvtxedg  28932  2wlkdlem1  29210  2pthd  29225  wlk2v2e  29441  3wlkdlem1  29443  3pthd  29458  konigsberg  29541  cnidOLD  29866  ip1ilem  30110  ipasslem10  30123  normlem6  30399  dfhnorm2  30406  h1de2i  30837  spansnji  30930  pjneli  31007  mayetes3i  31013  pjclem1  31479  mdslmd3i  31616  atabsi  31685  imadifxp  31863  dfdec100  32067  dpmul100  32094  dpmul1000  32096  dpmul4  32111  xrge00  32218  cyc2fv1  32311  cyc2fv2  32312  cyc3fv3  32329  opprlidlabs  32630  locfinref  32852  cnvordtrestixx  32924  raddcn  32940  rrhcn  33008  qqtopn  33022  esumpfinvallem  33103  sxbrsigalem1  33315  eulerpartgbij  33402  sgnneg  33570  hgt750lem2  33695  subfacp1lem1  34201  subfacval2  34209  quad3  34686  ptrest  36535  poimirlem3  36539  poimirlem8  36544  poimirlem15  36551  mblfinlem3  36575  ismblfin  36577  areacirc  36629  pmapglb  38689  dvh4dimN  40366  hdmapfval  40746  12gcd5e1  40916  sqdeccom12  41249  remul02  41326  mapfzcons1  41503  lmhmlnmsplit  41877  pwssplit4  41879  clcnvlem  42422  cnvrcl0  42424  sqrtcval2  42441  resqrtvalex  42444  imsqrtvalex  42445  iunrelexp0  42501  sumnnodd  44394  climinf2mpt  44478  climinfmpt  44479  dvnmul  44707  wallispilem4  44832  dirkertrigeqlem3  44864  fourierdlem24  44895  fourierdlem57  44927  fourierdlem58  44928  fourierdlem80  44950  fourierswlem  44994  fouriersw  44995  fouriercn  44996  subsaliuncl  45122  gsumge0cl  45135  sge0tsms  45144  caragenuncllem  45276  0ome  45293  hoidmvle  45364  ovolval3  45411  ovolval4lem1  45413  smfpimbor1lem2  45563  gbpart7  46483  gbpart9  46485  gbpart11  46486  nnsum3primes4  46504  xpiun  46584  opprrngb  46723  lindslinindsimp2lem5  47191  ackval42a  47431  aacllem  47896