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  4241  dfif3  4505  dfsn2  4604  prprc1  4731  diftpsn3  4768  ssunpr  4800  sstp  4802  unidif0  5317  xpindi  5799  xpindir  5800  dmcnvcnv  5899  rncnvcnv  5900  imainrect  6156  dfrn4  6177  predres  6314  fcoi1  6736  foimacnv  6819  f1ossf1o  7102  fsnunfv  7163  difex2  7738  dfoprab3  8035  offval22  8069  suppvalbr  8145  fvmpocurryd  8252  mapsnconst  8867  sbthlem8  9063  fiint  9283  fiintOLD  9284  ordtypecbv  9476  trcl  9687  rankxplim2  9839  infdju1  10149  cfval2  10219  itunitc  10380  ituniiun  10381  hsmex2  10392  ltexnq  10934  ixi  11813  zeo  12626  num0h  12667  dec10p  12698  fseq1p1m1  13565  cats1fvn  14830  s3fn  14883  fsumrelem  15779  ef0lem  16050  ef01bndlem  16158  sadcadd  16434  sadadd2  16436  3lcm2e6woprm  16591  mod2xnegi  17048  str0  17165  ressinbas  17221  mreexexlem4d  17614  0g0  18597  frmdplusg  18787  smndex1bas  18839  sgrp2nmndlem4  18861  sgrp2nmndlem5  18862  oppgplusfval  19286  symgsubmefmnd  19334  psgnsn  19456  psgnprfval1  19458  frgpnabllem1  19809  opprmulfval  20254  opprrngb  20261  opprringb  20263  opprunit  20292  00lsp  20893  chrval  21439  dsmmelbas  21654  ltbwe  21957  ply1plusgfvi  22132  mat2pmatfval  22616  unisngl  23420  qtopres  23591  ufildr  23824  oppgtmd  23990  tgioo  24690  tgqioo  24694  dveflem  25889  lhop1lem  25924  sincos4thpi  26428  coskpi  26438  cxpsqrtlem  26617  log2ublem1  26862  efrlim  26885  efrlimOLD  26886  basellem3  26999  bposlem9  27209  madeun  27801  precsexlem11  28125  0reno  28354  graop  28962  0grsubgr  29211  usgrfilem  29260  finsumvtxdg2ssteplem4  29482  wlkvtxedg  29578  2wlkdlem1  29861  2pthd  29876  wlk2v2e  30092  3wlkdlem1  30094  3pthd  30109  konigsberg  30192  cnidOLD  30517  ip1ilem  30761  ipasslem10  30774  normlem6  31050  dfhnorm2  31057  h1de2i  31488  spansnji  31581  pjneli  31658  mayetes3i  31664  pjclem1  32130  mdslmd3i  32267  atabsi  32336  imadifxp  32536  dfdec100  32761  sgnneg  32764  dpmul100  32823  dpmul1000  32825  dpmul4  32840  xrge00  32959  cyc2fv1  33084  cyc2fv2  33085  cyc3fv3  33102  opprlidlabs  33462  cos9thpiminplylem5  33782  locfinref  33837  cnvordtrestixx  33909  raddcn  33925  rrhcn  33993  qqtopn  34007  esumpfinvallem  34070  sxbrsigalem1  34282  eulerpartgbij  34369  hgt750lem2  34649  subfacp1lem1  35166  subfacval2  35174  quad3  35657  ptrest  37608  poimirlem3  37612  poimirlem8  37617  poimirlem15  37624  mblfinlem3  37648  ismblfin  37650  areacirc  37702  pmapglb  39759  dvh4dimN  41436  hdmapfval  41816  12gcd5e1  41986  sqdeccom12  42272  remul02  42388  mapfzcons1  42698  lmhmlnmsplit  43069  pwssplit4  43071  clcnvlem  43605  cnvrcl0  43607  sqrtcval2  43624  resqrtvalex  43627  imsqrtvalex  43628  iunrelexp0  43684  sumnnodd  45621  climinf2mpt  45705  climinfmpt  45706  dvnmul  45934  wallispilem4  46059  dirkertrigeqlem3  46091  fourierdlem24  46122  fourierdlem57  46154  fourierdlem58  46155  fourierdlem80  46177  fourierswlem  46221  fouriersw  46222  fouriercn  46223  subsaliuncl  46349  gsumge0cl  46362  sge0tsms  46371  caragenuncllem  46503  0ome  46520  hoidmvle  46591  ovolval3  46638  ovolval4lem1  46640  smfpimbor1lem2  46790  gbpart7  47758  gbpart9  47760  gbpart11  47761  nnsum3primes4  47779  xpiun  48136  lindslinindsimp2lem5  48441  ackval42a  48676  aacllem  49780