Theorem eqtr2i 2754

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 2753	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2739	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 2702

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

This theorem is referenced by:  3eqtrri  2758  3eqtr2ri  2760  dfun3  4242  dfif3  4506  dfsn2  4605  prprc1  4732  diftpsn3  4769  ssunpr  4801  sstp  4803  unidif0  5318  xpindi  5800  xpindir  5801  dmcnvcnv  5900  rncnvcnv  5901  imainrect  6157  dfrn4  6178  predres  6315  fcoi1  6737  foimacnv  6820  f1ossf1o  7103  fsnunfv  7164  difex2  7739  dfoprab3  8036  offval22  8070  suppvalbr  8146  fvmpocurryd  8253  mapsnconst  8868  sbthlem8  9064  fiint  9284  fiintOLD  9285  ordtypecbv  9477  trcl  9688  rankxplim2  9840  infdju1  10150  cfval2  10220  itunitc  10381  ituniiun  10382  hsmex2  10393  ltexnq  10935  ixi  11814  zeo  12627  num0h  12668  dec10p  12699  fseq1p1m1  13566  cats1fvn  14831  s3fn  14884  fsumrelem  15780  ef0lem  16051  ef01bndlem  16159  sadcadd  16435  sadadd2  16437  3lcm2e6woprm  16592  mod2xnegi  17049  str0  17166  ressinbas  17222  mreexexlem4d  17615  0g0  18598  frmdplusg  18788  smndex1bas  18840  sgrp2nmndlem4  18862  sgrp2nmndlem5  18863  oppgplusfval  19287  symgsubmefmnd  19335  psgnsn  19457  psgnprfval1  19459  frgpnabllem1  19810  opprmulfval  20255  opprrngb  20262  opprringb  20264  opprunit  20293  00lsp  20894  chrval  21440  dsmmelbas  21655  ltbwe  21958  ply1plusgfvi  22133  mat2pmatfval  22617  unisngl  23421  qtopres  23592  ufildr  23825  oppgtmd  23991  tgioo  24691  tgqioo  24695  dveflem  25890  lhop1lem  25925  sincos4thpi  26429  coskpi  26439  cxpsqrtlem  26618  log2ublem1  26863  efrlim  26886  efrlimOLD  26887  basellem3  27000  bposlem9  27210  madeun  27802  precsexlem11  28126  0reno  28355  graop  28963  0grsubgr  29212  usgrfilem  29261  finsumvtxdg2ssteplem4  29483  wlkvtxedg  29579  2wlkdlem1  29862  2pthd  29877  wlk2v2e  30093  3wlkdlem1  30095  3pthd  30110  konigsberg  30193  cnidOLD  30518  ip1ilem  30762  ipasslem10  30775  normlem6  31051  dfhnorm2  31058  h1de2i  31489  spansnji  31582  pjneli  31659  mayetes3i  31665  pjclem1  32131  mdslmd3i  32268  atabsi  32337  imadifxp  32537  dfdec100  32762  sgnneg  32765  dpmul100  32824  dpmul1000  32826  dpmul4  32841  xrge00  32960  cyc2fv1  33085  cyc2fv2  33086  cyc3fv3  33103  opprlidlabs  33463  cos9thpiminplylem5  33783  locfinref  33838  cnvordtrestixx  33910  raddcn  33926  rrhcn  33994  qqtopn  34008  esumpfinvallem  34071  sxbrsigalem1  34283  eulerpartgbij  34370  hgt750lem2  34650  subfacp1lem1  35173  subfacval2  35181  quad3  35664  ptrest  37620  poimirlem3  37624  poimirlem8  37629  poimirlem15  37636  mblfinlem3  37660  ismblfin  37662  areacirc  37714  pmapglb  39771  dvh4dimN  41448  hdmapfval  41828  12gcd5e1  41998  sqdeccom12  42284  remul02  42400  mapfzcons1  42712  lmhmlnmsplit  43083  pwssplit4  43085  clcnvlem  43619  cnvrcl0  43621  sqrtcval2  43638  resqrtvalex  43641  imsqrtvalex  43642  iunrelexp0  43698  sumnnodd  45635  climinf2mpt  45719  climinfmpt  45720  dvnmul  45948  wallispilem4  46073  dirkertrigeqlem3  46105  fourierdlem24  46136  fourierdlem57  46168  fourierdlem58  46169  fourierdlem80  46191  fourierswlem  46235  fouriersw  46236  fouriercn  46237  subsaliuncl  46363  gsumge0cl  46376  sge0tsms  46385  caragenuncllem  46517  0ome  46534  hoidmvle  46605  ovolval3  46652  ovolval4lem1  46654  smfpimbor1lem2  46804  gbpart7  47772  gbpart9  47774  gbpart11  47775  nnsum3primes4  47793  xpiun  48150  lindslinindsimp2lem5  48455  ackval42a  48690  aacllem  49794