Theorem eqtr2i 2753

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  3eqtrri  2757  3eqtr2ri  2759  dfun3  4239  dfif3  4503  dfsn2  4602  prprc1  4729  diftpsn3  4766  ssunpr  4798  sstp  4800  unidif0  5315  xpindi  5797  xpindir  5798  dmcnvcnv  5897  rncnvcnv  5898  imainrect  6154  dfrn4  6175  predres  6312  fcoi1  6734  foimacnv  6817  f1ossf1o  7100  fsnunfv  7161  difex2  7736  dfoprab3  8033  offval22  8067  suppvalbr  8143  fvmpocurryd  8250  mapsnconst  8865  sbthlem8  9058  fiint  9277  fiintOLD  9278  ordtypecbv  9470  trcl  9681  rankxplim2  9833  infdju1  10143  cfval2  10213  itunitc  10374  ituniiun  10375  hsmex2  10386  ltexnq  10928  ixi  11807  zeo  12620  num0h  12661  dec10p  12692  fseq1p1m1  13559  cats1fvn  14824  s3fn  14877  fsumrelem  15773  ef0lem  16044  ef01bndlem  16152  sadcadd  16428  sadadd2  16430  3lcm2e6woprm  16585  mod2xnegi  17042  str0  17159  ressinbas  17215  mreexexlem4d  17608  0g0  18591  frmdplusg  18781  smndex1bas  18833  sgrp2nmndlem4  18855  sgrp2nmndlem5  18856  oppgplusfval  19280  symgsubmefmnd  19328  psgnsn  19450  psgnprfval1  19452  frgpnabllem1  19803  opprmulfval  20248  opprrngb  20255  opprringb  20257  opprunit  20286  00lsp  20887  chrval  21433  dsmmelbas  21648  ltbwe  21951  ply1plusgfvi  22126  mat2pmatfval  22610  unisngl  23414  qtopres  23585  ufildr  23818  oppgtmd  23984  tgioo  24684  tgqioo  24688  dveflem  25883  lhop1lem  25918  sincos4thpi  26422  coskpi  26432  cxpsqrtlem  26611  log2ublem1  26856  efrlim  26879  efrlimOLD  26880  basellem3  26993  bposlem9  27203  madeun  27795  precsexlem11  28119  0reno  28348  graop  28956  0grsubgr  29205  usgrfilem  29254  finsumvtxdg2ssteplem4  29476  wlkvtxedg  29572  2wlkdlem1  29855  2pthd  29870  wlk2v2e  30086  3wlkdlem1  30088  3pthd  30103  konigsberg  30186  cnidOLD  30511  ip1ilem  30755  ipasslem10  30768  normlem6  31044  dfhnorm2  31051  h1de2i  31482  spansnji  31575  pjneli  31652  mayetes3i  31658  pjclem1  32124  mdslmd3i  32261  atabsi  32330  imadifxp  32530  dfdec100  32755  sgnneg  32758  dpmul100  32817  dpmul1000  32819  dpmul4  32834  xrge00  32953  cyc2fv1  33078  cyc2fv2  33079  cyc3fv3  33096  opprlidlabs  33456  cos9thpiminplylem5  33776  locfinref  33831  cnvordtrestixx  33903  raddcn  33919  rrhcn  33987  qqtopn  34001  esumpfinvallem  34064  sxbrsigalem1  34276  eulerpartgbij  34363  hgt750lem2  34643  subfacp1lem1  35166  subfacval2  35174  quad3  35657  ptrest  37613  poimirlem3  37617  poimirlem8  37622  poimirlem15  37629  mblfinlem3  37653  ismblfin  37655  areacirc  37707  pmapglb  39764  dvh4dimN  41441  hdmapfval  41821  12gcd5e1  41991  sqdeccom12  42277  remul02  42393  mapfzcons1  42705  lmhmlnmsplit  43076  pwssplit4  43078  clcnvlem  43612  cnvrcl0  43614  sqrtcval2  43631  resqrtvalex  43634  imsqrtvalex  43635  iunrelexp0  43691  sumnnodd  45628  climinf2mpt  45712  climinfmpt  45713  dvnmul  45941  wallispilem4  46066  dirkertrigeqlem3  46098  fourierdlem24  46129  fourierdlem57  46161  fourierdlem58  46162  fourierdlem80  46184  fourierswlem  46228  fouriersw  46229  fouriercn  46230  subsaliuncl  46356  gsumge0cl  46369  sge0tsms  46378  caragenuncllem  46510  0ome  46527  hoidmvle  46598  ovolval3  46645  ovolval4lem1  46647  smfpimbor1lem2  46797  gbpart7  47768  gbpart9  47770  gbpart11  47771  nnsum3primes4  47789  xpiun  48146  lindslinindsimp2lem5  48451  ackval42a  48686  aacllem  49790