Theorem eqtr2i 2829

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

Syntax hints:   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  3eqtrri  2833  3eqtr2ri  2835  dfun3  4067  dfif3  4293  dfsn2  4383  prprc1  4491  diftpsn3  4523  ssunpr  4553  sstp  4555  unidif0  5030  pwundif  5216  xpindi  5457  xpindir  5458  dmcnvcnv  5549  rncnvcnv  5550  imainrect  5786  dfrn4  5806  fcoi1  6289  foimacnv  6366  f1ossf1o  6614  fsnunfv  6674  difex2  7195  dfoprab3  7452  offval22  7483  fvmpt2curryd  7628  mapsnconst  8136  sbthlem8  8312  fiint  8472  ordtypecbv  8657  ruv  8742  trcl  8847  rankxplim2  8986  infcda1  9296  cfval2  9363  itunitc  9524  ituniiun  9525  hsmex2  9536  ltexnq  10078  ixi  10937  zeo  11725  num0h  11767  dec10p  11798  fseq1p1m1  12633  cats1fvn  13823  s3fn  13876  fsumrelem  14757  ef0lem  15025  ef01bndlem  15130  sadcadd  15395  sadadd2  15397  3lcm2e6woprm  15543  mod2xnegi  15988  decexp2  15992  str0  16118  ressinbas  16143  mreexexlem4d  16508  0g0  17464  frmdplusg  17592  sgrp2nmndlem4  17616  sgrp2nmndlem5  17617  oppgplusfval  17975  psgnsn  18137  psgnprfval1  18139  frgpnabllem1  18473  opprmulfval  18823  opprringb  18830  opprunit  18859  00lsp  19184  psrmulr  19589  ltbwe  19677  ply1plusgfvi  19816  chrval  20077  dsmmelbas  20290  mat2pmatfval  20738  unisngl  21541  qtopres  21712  ufildr  21945  oppgtmd  22111  tgioo  22809  tgqioo  22813  dveflem  23955  lhop1lem  23989  sincos4thpi  24479  coskpi  24486  cxpsqrtlem  24661  log2ublem1  24886  efrlim  24909  basellem3  25022  bposlem9  25230  graop  26134  0grsubgr  26385  usgrfilem  26434  finsumvtxdg2ssteplem4  26671  wlkvtxedg  26767  2wlkdlem1  27064  2pthd  27079  wlk2v2e  27329  3wlkdlem1  27331  3pthd  27346  konigsberg  27429  cnidOLD  27764  ip1ilem  28008  ipasslem10  28021  normlem6  28299  dfhnorm2  28306  h1de2i  28739  spansnji  28832  pjneli  28909  mayetes3i  28915  pjclem1  29381  mdslmd3i  29518  atabsi  29587  imadifxp  29738  dfdec100  29902  dpmul100  29929  dpmul1000  29931  dpmul4  29946  xrge00  30010  locfinref  30232  cnvordtrestixx  30283  raddcn  30299  rrhcn  30365  qqtopn  30379  esumpfinvallem  30460  isrnsigaOLD  30499  sxbrsigalem1  30671  eulerpartgbij  30758  sgnneg  30926  hgt750lem2  31054  subfacp1lem1  31482  subfacval2  31490  quad3  31884  ptrest  33719  poimirlem3  33723  poimirlem8  33728  poimirlem15  33735  mblfinlem3  33759  ismblfin  33761  areacirc  33815  pmapglb  35548  dvh4dimN  37225  hdmapfval  37605  mapfzcons1  37779  lmhmlnmsplit  38155  pwssplit4  38157  clcnvlem  38427  cnvrcl0  38429  iunrelexp0  38491  sumnnodd  40339  climinf2mpt  40423  climinfmpt  40424  dvnmul  40635  wallispilem4  40761  dirkertrigeqlem3  40793  fourierdlem24  40824  fourierdlem57  40856  fourierdlem58  40857  fourierdlem80  40879  fourierswlem  40923  fouriersw  40924  fouriercn  40925  subsaliuncl  41052  gsumge0cl  41064  sge0tsms  41073  caragenuncllem  41205  0ome  41222  hoidmvle  41293  ovolval3  41340  ovolval4lem1  41342  smfpimbor1lem2  41485  gbpart7  42227  gbpart9  42229  gbpart11  42230  nnsum3primes4  42248  xpiun  42331  lindslinindsimp2lem5  42816  aacllem  43115