Theorem eqtr2i 2757

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

Syntax hints:   = wceq 1541

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  3eqtrri  2761  3eqtr2ri  2763  dfun3  4225  dfif3  4491  dfsn2  4590  prprc1  4719  diftpsn3  4755  ssunpr  4787  sstp  4789  unidif0  5302  xpindi  5779  xpindir  5780  dmcnvcnv  5879  rncnvcnv  5880  imainrect  6136  dfrn4  6157  predres  6294  fcoi1  6705  foimacnv  6788  f1ossf1o  7070  fsnunfv  7130  difex2  7702  dfoprab3  7995  offval22  8027  suppvalbr  8103  fvmpocurryd  8210  mapsnconst  8826  sbthlem8  9018  fiint  9222  ordtypecbv  9414  trcl  9629  rankxplim2  9784  infdju1  10092  cfval2  10162  itunitc  10323  ituniiun  10324  hsmex2  10335  ltexnq  10877  ixi  11757  zeo  12569  num0h  12610  dec10p  12641  fseq1p1m1  13505  cats1fvn  14772  s3fn  14825  fsumrelem  15721  ef0lem  15992  ef01bndlem  16100  sadcadd  16376  sadadd2  16378  3lcm2e6woprm  16533  mod2xnegi  16990  str0  17107  ressinbas  17163  mreexexlem4d  17561  0g0  18580  frmdplusg  18770  smndex1bas  18822  sgrp2nmndlem4  18844  sgrp2nmndlem5  18845  oppgplusfval  19268  symgsubmefmnd  19318  psgnsn  19440  psgnprfval1  19442  frgpnabllem1  19793  opprmulfval  20266  opprrngb  20273  opprringb  20275  opprunit  20304  00lsp  20923  chrval  21469  dsmmelbas  21685  ltbwe  21990  ply1plusgfvi  22173  mat2pmatfval  22658  unisngl  23462  qtopres  23633  ufildr  23866  oppgtmd  24032  tgioo  24731  tgqioo  24735  dveflem  25930  lhop1lem  25965  sincos4thpi  26469  coskpi  26479  cxpsqrtlem  26658  log2ublem1  26903  efrlim  26926  efrlimOLD  26927  basellem3  27040  bposlem9  27250  madeun  27849  precsexlem11  28175  0reno  28419  graop  29028  0grsubgr  29277  usgrfilem  29326  finsumvtxdg2ssteplem4  29548  wlkvtxedg  29643  2wlkdlem1  29924  2pthd  29939  wlk2v2e  30158  3wlkdlem1  30160  3pthd  30175  konigsberg  30258  cnidOLD  30583  ip1ilem  30827  ipasslem10  30840  normlem6  31116  dfhnorm2  31123  h1de2i  31554  spansnji  31647  pjneli  31724  mayetes3i  31730  pjclem1  32196  mdslmd3i  32333  atabsi  32402  imadifxp  32602  dfdec100  32839  sgnneg  32842  dpmul100  32906  dpmul1000  32908  dpmul4  32923  xrge00  33024  cyc2fv1  33131  cyc2fv2  33132  cyc3fv3  33149  opprlidlabs  33494  vieta  33664  cos9thpiminplylem5  33871  locfinref  33926  cnvordtrestixx  33998  raddcn  34014  rrhcn  34082  qqtopn  34096  esumpfinvallem  34159  sxbrsigalem1  34370  eulerpartgbij  34457  hgt750lem2  34737  subfacp1lem1  35295  subfacval2  35303  quad3  35786  ptrest  37732  poimirlem3  37736  poimirlem8  37741  poimirlem15  37748  mblfinlem3  37772  ismblfin  37774  areacirc  37826  pmapglb  39942  dvh4dimN  41619  hdmapfval  41999  12gcd5e1  42169  sqdeccom12  42459  remul02  42575  mapfzcons1  42874  lmhmlnmsplit  43244  pwssplit4  43246  clcnvlem  43780  cnvrcl0  43782  sqrtcval2  43799  resqrtvalex  43802  imsqrtvalex  43803  iunrelexp0  43859  sumnnodd  45792  climinf2mpt  45874  climinfmpt  45875  dvnmul  46103  wallispilem4  46228  dirkertrigeqlem3  46260  fourierdlem24  46291  fourierdlem57  46323  fourierdlem58  46324  fourierdlem80  46346  fourierswlem  46390  fouriersw  46391  fouriercn  46392  subsaliuncl  46518  gsumge0cl  46531  sge0tsms  46540  caragenuncllem  46672  0ome  46689  hoidmvle  46760  ovolval3  46807  ovolval4lem1  46809  smfpimbor1lem2  46959  gbpart7  47929  gbpart9  47931  gbpart11  47932  nnsum3primes4  47950  gpg5edgnedg  48292  xpiun  48320  lindslinindsimp2lem5  48624  ackval42a  48859  aacllem  49962