Theorem eqtr2i 2784

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  3eqtrri  2788  3eqtr2ri  2790  dfun3  4221  dfif3  4496  dfsn2  4593  prprc1  4722  diftpsn3  4761  ssunpr  4788  sstp  4790  unidif0OLD  5321  xpindi  5809  xpindir  5810  dmcnvcnv  5914  rncnvcnv  5915  imainrect  6172  dfrn4  6196  imadifssranOLD  6202  predres  6342  fcoi1  6757  foimacnv  6843  f1ossf1o  7130  fsnunfv  7193  difex2  7775  dfoprab3  8066  offval22  8100  suppvalbrOLD  8185  fvmpocurryd  8292  mapsnconst  8924  sbthlem8  9117  fiint  9322  ordtypecbv  9515  trcl  9733  rankxplim2  9901  infdju1  10272  cfval2  10342  itunitc  10503  ituniiun  10504  hsmex2  10515  ltexnq  11064  ixi  11949  zeo  12789  num0h  12830  dec10p  12866  fseq1p1m1  13736  cats1fvn  15014  s3fn  15068  sgnneg  15259  fsumrelem  15980  ef0lem  16250  ef01bndlem  16358  sadcadd  16634  sadadd2  16636  3lcm2e6woprm  16796  mod2xnegi  17255  str0  17373  ressinbas  17429  mreexexlem4d  17827  0g0  18850  frmdplusg  19056  smndex1bas  19111  sgrp2nmndlem4  19133  sgrp2nmndlem5  19134  oppgplusfval  19568  symgsubmefmnd  19618  psgnsn  19740  psgnprfval1  19742  frgpnabllem1  20093  opprmulfval  20575  opprrngb  20582  opprringb  20584  opprunit  20613  isdrng3lem1  21011  00lsp  21262  rspvalint  21529  chrval  21835  dsmmelbas  22051  ltbwe  22359  ply1plusgfvi  22565  mat2pmatfval  23047  unisngl  23852  qtopres  24023  ufildr  24256  oppgtmd  24422  tgioo  25121  tgqioo  25125  dveflem  26305  lhop1lem  26339  sincos4thpi  26848  coskpi  26857  cxpsqrtlem  27036  log2ublem1  27280  efrlim  27303  basellem3  27416  bposlem9  27625  madeun  28276  precsexlem11  28609  graop  29613  0grsubgr  29865  usgrfilem  29914  finsumvtxdg2ssteplem4  30135  wlkvtxedg  30230  2wlkdlem1  30520  2pthd  30535  wlk2v2e  30764  3wlkdlem1  30766  3pthd  30781  konigsberg  30864  cnidOLD  31190  ip1ilem  31434  ipasslem10  31447  normlem6  31723  dfhnorm2  31730  h1de2i  32161  spansnji  32254  pjneli  32331  mayetes3i  32337  pjclem1  32803  mdslmd3i  32940  atabsi  33009  imadifxp  33243  dfdec100  33468  dpmul100  33510  dpmul1000  33512  dpmul4  33527  xrge00  33622  cyc2fv1  33729  cyc2fv2  33730  cyc3fv3  33747  opprlidlabs  34056  vieta  34259  cos9thpiminplylem5  34465  locfinref  34520  cnvordtrestixx  34592  raddcn  34608  rrhcn  34676  qqtopn  34690  esumpfinvallem  34753  sxbrsigalem1  34964  eulerpartgbij  35051  hgt750lem2  35328  j0ltalephlem  35947  subfacp1lem1  36031  subfacval2  36039  quad3  36522  ptrest  38631  poimirlem3  38635  poimirlem8  38640  poimirlem15  38647  mblfinlem3  38671  ismblfin  38673  areacirc  38725  pmapglb  40921  dvh4dimN  42598  hdmapfval  42978  12gcd5e1  43147  sqdeccom12  43440  remul02  43550  mapfzcons1  43822  lmhmlnmsplit  44183  pwssplit4  44185  clcnvlem  44717  cnvrcl0  44719  sqrtcval2  44736  resqrtvalex  44739  imsqrtvalex  44740  iunrelexp0  44796  sumnnodd  46736  climinf2mpt  46818  climinfmpt  46819  dvnmul  47047  wallispilem4  47172  dirkertrigeqlem3  47204  fourierdlem24  47235  fourierdlem57  47267  fourierdlem58  47268  fourierdlem80  47290  fourierswlem  47334  fouriersw  47335  fouriercn  47336  subsaliuncl  47462  gsumge0cl  47475  sge0tsms  47484  caragenuncllem  47616  0ome  47633  hoidmvle  47704  ovolval3  47751  ovolval4lem1  47753  smfpimbor1lem2  47903  goldpolyfactor  48021  sqrtnpoly  48037  gbpart7  48959  gbpart9  48961  gbpart11  48962  nnsum3primes4  48980  gpg5edgnedg  49322  xpiun  49350  lindslinindsimp2lem5  49668  ackval42a  49903  aacllem  51108