Theorem eqtr2i 2763

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

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  3eqtrri  2767  3eqtr2ri  2769  dfun3  4204  dfif3  4469  dfsn2  4568  prprc1  4697  diftpsn3  4735  ssunpr  4765  sstp  4767  unidif0OLD  5289  xpindi  5775  xpindir  5776  dmcnvcnv  5875  rncnvcnv  5876  imainrect  6132  dfrn4  6153  predres  6290  fcoi1  6701  foimacnv  6784  f1ossf1o  7070  fsnunfv  7131  difex2  7703  dfoprab3  7996  offval22  8027  suppvalbr  8104  fvmpocurryd  8211  mapsnconst  8830  sbthlem8  9022  fiint  9227  ordtypecbv  9422  trcl  9640  rankxplim2  9795  infdju1  10103  cfval2  10173  itunitc  10334  ituniiun  10335  hsmex2  10346  ltexnq  10889  ixi  11770  zeo  12606  num0h  12647  dec10p  12678  fseq1p1m1  13543  cats1fvn  14811  s3fn  14864  fsumrelem  15761  ef0lem  16034  ef01bndlem  16142  sadcadd  16418  sadadd2  16420  3lcm2e6woprm  16575  mod2xnegi  17033  str0  17150  ressinbas  17206  mreexexlem4d  17604  0g0  18623  frmdplusg  18813  smndex1bas  18868  sgrp2nmndlem4  18890  sgrp2nmndlem5  18891  oppgplusfval  19314  symgsubmefmnd  19364  psgnsn  19486  psgnprfval1  19488  frgpnabllem1  19839  opprmulfval  20310  opprrngb  20317  opprringb  20319  opprunit  20348  00lsp  20971  chrval  21498  dsmmelbas  21714  ltbwe  22020  ply1plusgfvi  22226  mat2pmatfval  22706  unisngl  23510  qtopres  23681  ufildr  23914  oppgtmd  24080  tgioo  24779  tgqioo  24783  dveflem  25964  lhop1lem  25998  sincos4thpi  26495  coskpi  26505  cxpsqrtlem  26684  log2ublem1  26928  efrlim  26951  basellem3  27064  bposlem9  27273  madeun  27894  precsexlem11  28227  graop  29116  0grsubgr  29365  usgrfilem  29414  finsumvtxdg2ssteplem4  29635  wlkvtxedg  29730  2wlkdlem1  30011  2pthd  30026  wlk2v2e  30245  3wlkdlem1  30247  3pthd  30262  konigsberg  30345  cnidOLD  30671  ip1ilem  30915  ipasslem10  30928  normlem6  31204  dfhnorm2  31211  h1de2i  31642  spansnji  31735  pjneli  31812  mayetes3i  31818  pjclem1  32284  mdslmd3i  32421  atabsi  32490  imadifxp  32690  dfdec100  32922  sgnneg  32925  dpmul100  32975  dpmul1000  32977  dpmul4  32992  xrge00  33093  cyc2fv1  33202  cyc2fv2  33203  cyc3fv3  33220  opprlidlabs  33568  vieta  33764  cos9thpiminplylem5  33970  locfinref  34025  cnvordtrestixx  34097  raddcn  34113  rrhcn  34181  qqtopn  34195  esumpfinvallem  34258  sxbrsigalem1  34469  eulerpartgbij  34556  hgt750lem2  34836  subfacp1lem1  35407  subfacval2  35415  quad3  35898  ptrest  37986  poimirlem3  37990  poimirlem8  37995  poimirlem15  38002  mblfinlem3  38026  ismblfin  38028  areacirc  38080  pmapglb  40262  dvh4dimN  41939  hdmapfval  42319  12gcd5e1  42488  sqdeccom12  42766  remul02  42882  mapfzcons1  43166  lmhmlnmsplit  43532  pwssplit4  43534  clcnvlem  44067  cnvrcl0  44069  sqrtcval2  44086  resqrtvalex  44089  imsqrtvalex  44090  iunrelexp0  44146  sumnnodd  46075  climinf2mpt  46157  climinfmpt  46158  dvnmul  46386  wallispilem4  46511  dirkertrigeqlem3  46543  fourierdlem24  46574  fourierdlem57  46606  fourierdlem58  46607  fourierdlem80  46629  fourierswlem  46673  fouriersw  46674  fouriercn  46675  subsaliuncl  46801  gsumge0cl  46814  sge0tsms  46823  caragenuncllem  46955  0ome  46972  hoidmvle  47043  ovolval3  47090  ovolval4lem1  47092  smfpimbor1lem2  47242  gbpart7  48258  gbpart9  48260  gbpart11  48261  nnsum3primes4  48279  gpg5edgnedg  48621  xpiun  48649  lindslinindsimp2lem5  48953  ackval42a  49188  aacllem  50291