Theorem eqtr2i 2787

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  3eqtrri  2791  3eqtr2ri  2793  dfun3  4224  dfif3  4500  dfsn2  4597  prprc1  4726  diftpsn3  4765  ssunpr  4792  sstp  4794  unidif0OLD  5327  xpindi  5818  xpindir  5819  dmcnvcnv  5925  rncnvcnv  5926  imainrect  6189  dfrn4  6213  imadifssranOLD  6219  predres  6366  fcoi1  6784  foimacnv  6870  f1ossf1o  7159  fsnunfv  7221  difex2  7804  dfoprab3  8098  offval22  8132  suppvalbrOLD  8217  fvmpocurryd  8324  mapsnconst  8956  sbthlem8  9149  fiint  9354  ordtypecbv  9546  trcl  9764  rankxplim2  9932  infdju1  10305  cfval2  10375  itunitc  10536  ituniiun  10537  hsmex2  10548  ltexnq  11097  ixi  11983  zeo  12823  num0h  12864  dec10p  12900  fseq1p1m1  13770  cats1fvn  15049  s3fn  15103  sgnneg  15294  fsumrelem  16015  ef0lem  16285  ef01bndlem  16393  sadcadd  16669  sadadd2  16671  3lcm2e6woprm  16831  mod2xnegi  17290  str0  17408  ressinbas  17464  mreexexlem4d  17862  0g0  18885  frmdplusg  19091  smndex1bas  19146  sgrp2nmndlem4  19168  sgrp2nmndlem5  19169  oppgplusfval  19604  symgsubmefmnd  19654  psgnsn  19776  psgnprfval1  19778  frgpnabllem1  20129  opprmulfval  20611  opprrngb  20618  opprringb  20620  opprunit  20649  isdrng3lem1  21047  00lsp  21298  rspvalint  21565  chrval  21873  dsmmelbas  22089  ltbwe  22397  ply1plusgfvi  22603  mat2pmatfval  23085  unisngl  23890  qtopres  24061  ufildr  24294  oppgtmd  24460  tgioo  25159  tgqioo  25163  dveflem  26343  lhop1lem  26377  sincos4thpi  26888  coskpi  26897  cxpsqrtlem  27076  log2ublem1  27320  efrlim  27343  basellem3  27456  bposlem9  27665  madeun  28316  precsexlem11  28649  graop  29653  0grsubgr  29905  usgrfilem  29954  finsumvtxdg2ssteplem4  30175  wlkvtxedg  30270  2wlkdlem1  30560  2pthd  30575  wlk2v2e  30804  3wlkdlem1  30806  3pthd  30821  konigsberg  30904  cnidOLD  31230  ip1ilem  31474  ipasslem10  31487  normlem6  31763  dfhnorm2  31770  h1de2i  32201  spansnji  32294  pjneli  32371  mayetes3i  32377  pjclem1  32843  mdslmd3i  32980  atabsi  33049  imadifxp  33283  dfdec100  33507  dpmul100  33549  dpmul1000  33551  dpmul4  33566  xrge00  33664  cyc2fv1  33771  cyc2fv2  33772  cyc3fv3  33789  opprlidlabs  34106  vieta  34316  cos9thpiminplylem5  34522  locfinref  34577  cnvordtrestixx  34649  raddcn  34665  rrhcn  34733  qqtopn  34747  esumpfinvallem  34810  sxbrsigalem1  35021  eulerpartgbij  35108  hgt750lem2  35385  j0ltalephlem  36041  subfacp1lem1  36145  subfacval2  36153  quad3  36636  ptrest  38798  poimirlem3  38802  poimirlem8  38807  poimirlem15  38814  mblfinlem3  38838  ismblfin  38840  areacirc  38892  pmapglb  41086  dvh4dimN  42763  hdmapfval  43143  12gcd5e1  43312  sqdeccom12  43606  remul02  43716  mapfzcons1  43988  lmhmlnmsplit  44349  pwssplit4  44351  clcnvlem  44878  cnvrcl0  44880  sqrtcval2  44897  resqrtvalex  44900  imsqrtvalex  44901  iunrelexp0  44957  sumnnodd  46909  climinf2mpt  46991  climinfmpt  46992  dvnmul  47220  wallispilem4  47345  dirkertrigeqlem3  47377  fourierdlem24  47408  fourierdlem57  47440  fourierdlem58  47441  fourierdlem80  47463  fourierswlem  47507  fouriersw  47508  fouriercn  47509  subsaliuncl  47635  gsumge0cl  47648  sge0tsms  47657  caragenuncllem  47789  0ome  47806  hoidmvle  47877  ovolval3  47924  ovolval4lem1  47926  smfpimbor1lem2  48076  goldpolyfactor  48194  sqrtnpoly  48210  gbpart7  49132  gbpart9  49134  gbpart11  49135  nnsum3primes4  49153  gpg5edgnedg  49495  xpiun  49523  bruval2  49741  lindslinindsimp2lem5  49899  ackval42a  50134  aacllem  51361