Theorem eqtr2i 2760

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 2759	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2740	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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  3eqtrri  2764  3eqtr2ri  2766  dfun3  4230  dfif3  4505  dfsn2  4604  prprc1  4731  diftpsn3  4767  ssunpr  4797  sstp  4799  unidif0  5320  xpindi  5794  xpindir  5795  dmcnvcnv  5893  rncnvcnv  5894  imainrect  6138  dfrn4  6159  predres  6298  fcoi1  6721  foimacnv  6806  f1ossf1o  7079  fsnunfv  7138  difex2  7699  dfoprab3  7991  offval22  8025  fvmpocurryd  8207  mapsnconst  8837  sbthlem8  9041  fiint  9275  ordtypecbv  9462  trcl  9673  rankxplim2  9825  infdju1  10134  cfval2  10205  itunitc  10366  ituniiun  10367  hsmex2  10378  ltexnq  10920  ixi  11793  zeo  12598  num0h  12639  dec10p  12670  fseq1p1m1  13525  cats1fvn  14759  s3fn  14812  fsumrelem  15703  ef0lem  15972  ef01bndlem  16077  sadcadd  16349  sadadd2  16351  3lcm2e6woprm  16502  mod2xnegi  16954  decexp2  16958  str0  17072  ressinbas  17140  mreexexlem4d  17541  0g0  18533  frmdplusg  18678  smndex1bas  18730  sgrp2nmndlem4  18752  sgrp2nmndlem5  18753  oppgplusfval  19140  symgsubmefmnd  19194  psgnsn  19316  psgnprfval1  19318  frgpnabllem1  19665  opprmulfval  20065  opprringb  20075  opprunit  20104  00lsp  20499  chrval  20965  dsmmelbas  21182  ltbwe  21482  ply1plusgfvi  21650  mat2pmatfval  22109  unisngl  22915  qtopres  23086  ufildr  23319  oppgtmd  23485  tgioo  24196  tgqioo  24200  dveflem  25380  lhop1lem  25414  sincos4thpi  25907  coskpi  25916  cxpsqrtlem  26094  log2ublem1  26333  efrlim  26356  basellem3  26469  bposlem9  26677  madeun  27256  graop  28043  0grsubgr  28289  usgrfilem  28338  finsumvtxdg2ssteplem4  28559  wlkvtxedg  28655  2wlkdlem1  28933  2pthd  28948  wlk2v2e  29164  3wlkdlem1  29166  3pthd  29181  konigsberg  29264  cnidOLD  29587  ip1ilem  29831  ipasslem10  29844  normlem6  30120  dfhnorm2  30127  h1de2i  30558  spansnji  30651  pjneli  30728  mayetes3i  30734  pjclem1  31200  mdslmd3i  31337  atabsi  31406  imadifxp  31586  dfdec100  31796  dpmul100  31823  dpmul1000  31825  dpmul4  31840  xrge00  31947  cyc2fv1  32040  cyc2fv2  32041  cyc3fv3  32058  locfinref  32511  cnvordtrestixx  32583  raddcn  32599  rrhcn  32667  qqtopn  32681  esumpfinvallem  32762  sxbrsigalem1  32974  eulerpartgbij  33061  sgnneg  33229  hgt750lem2  33354  subfacp1lem1  33860  subfacval2  33868  quad3  34345  ptrest  36150  poimirlem3  36154  poimirlem8  36159  poimirlem15  36166  mblfinlem3  36190  ismblfin  36192  areacirc  36244  pmapglb  38306  dvh4dimN  39983  hdmapfval  40363  12gcd5e1  40533  sqdeccom12  40861  remul02  40932  mapfzcons1  41098  lmhmlnmsplit  41472  pwssplit4  41474  clcnvlem  42017  cnvrcl0  42019  sqrtcval2  42036  resqrtvalex  42039  imsqrtvalex  42040  iunrelexp0  42096  sumnnodd  43991  climinf2mpt  44075  climinfmpt  44076  dvnmul  44304  wallispilem4  44429  dirkertrigeqlem3  44461  fourierdlem24  44492  fourierdlem57  44524  fourierdlem58  44525  fourierdlem80  44547  fourierswlem  44591  fouriersw  44592  fouriercn  44593  subsaliuncl  44719  gsumge0cl  44732  sge0tsms  44741  caragenuncllem  44873  0ome  44890  hoidmvle  44961  ovolval3  45008  ovolval4lem1  45010  smfpimbor1lem2  45160  gbpart7  46079  gbpart9  46081  gbpart11  46082  nnsum3primes4  46100  xpiun  46180  lindslinindsimp2lem5  46663  ackval42a  46903  aacllem  47368