Theorem eqtr2i 2767

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  3eqtrri  2771  3eqtr2ri  2773  dfun3  4196  dfif3  4470  dfsn2  4571  prprc1  4698  diftpsn3  4732  ssunpr  4762  sstp  4764  unidif0  5277  pwundifOLD  5477  xpindi  5731  xpindir  5732  dmcnvcnv  5831  rncnvcnv  5832  imainrect  6073  dfrn4  6094  fcoi1  6632  foimacnv  6717  f1ossf1o  6982  fsnunfv  7041  difex2  7588  dfoprab3  7867  offval22  7899  fvmpocurryd  8058  mapsnconst  8638  sbthlem8  8830  fiint  9021  ordtypecbv  9206  trcl  9417  rankxplim2  9569  infdju1  9876  cfval2  9947  itunitc  10108  ituniiun  10109  hsmex2  10120  ltexnq  10662  ixi  11534  zeo  12336  num0h  12378  dec10p  12409  fseq1p1m1  13259  cats1fvn  14499  s3fn  14552  fsumrelem  15447  ef0lem  15716  ef01bndlem  15821  sadcadd  16093  sadadd2  16095  3lcm2e6woprm  16248  mod2xnegi  16700  decexp2  16704  str0  16818  ressinbas  16881  mreexexlem4d  17273  0g0  18263  frmdplusg  18408  smndex1bas  18460  sgrp2nmndlem4  18482  sgrp2nmndlem5  18483  oppgplusfval  18867  symgsubmefmnd  18921  psgnsn  19043  psgnprfval1  19045  frgpnabllem1  19389  opprmulfval  19779  opprringb  19789  opprunit  19818  00lsp  20158  chrval  20641  dsmmelbas  20856  ltbwe  21155  ply1plusgfvi  21323  mat2pmatfval  21780  unisngl  22586  qtopres  22757  ufildr  22990  oppgtmd  23156  tgioo  23865  tgqioo  23869  dveflem  25048  lhop1lem  25082  sincos4thpi  25575  coskpi  25584  cxpsqrtlem  25762  log2ublem1  26001  efrlim  26024  basellem3  26137  bposlem9  26345  graop  27302  0grsubgr  27548  usgrfilem  27597  finsumvtxdg2ssteplem4  27818  wlkvtxedg  27913  2wlkdlem1  28191  2pthd  28206  wlk2v2e  28422  3wlkdlem1  28424  3pthd  28439  konigsberg  28522  cnidOLD  28845  ip1ilem  29089  ipasslem10  29102  normlem6  29378  dfhnorm2  29385  h1de2i  29816  spansnji  29909  pjneli  29986  mayetes3i  29992  pjclem1  30458  mdslmd3i  30595  atabsi  30664  imadifxp  30841  dfdec100  31046  dpmul100  31073  dpmul1000  31075  dpmul4  31090  xrge00  31197  cyc2fv1  31290  cyc2fv2  31291  cyc3fv3  31308  locfinref  31693  cnvordtrestixx  31765  raddcn  31781  rrhcn  31847  qqtopn  31861  esumpfinvallem  31942  sxbrsigalem1  32152  eulerpartgbij  32239  sgnneg  32407  hgt750lem2  32532  subfacp1lem1  33041  subfacval2  33049  quad3  33528  madeun  33993  ptrest  35703  poimirlem3  35707  poimirlem8  35712  poimirlem15  35719  mblfinlem3  35743  ismblfin  35745  areacirc  35797  pmapglb  37711  dvh4dimN  39388  hdmapfval  39768  12gcd5e1  39939  sqdeccom12  40238  remul02  40309  mapfzcons1  40455  lmhmlnmsplit  40828  pwssplit4  40830  clcnvlem  41120  cnvrcl0  41122  sqrtcval2  41139  resqrtvalex  41142  imsqrtvalex  41143  iunrelexp0  41199  sumnnodd  43061  climinf2mpt  43145  climinfmpt  43146  dvnmul  43374  wallispilem4  43499  dirkertrigeqlem3  43531  fourierdlem24  43562  fourierdlem57  43594  fourierdlem58  43595  fourierdlem80  43617  fourierswlem  43661  fouriersw  43662  fouriercn  43663  subsaliuncl  43787  gsumge0cl  43799  sge0tsms  43808  caragenuncllem  43940  0ome  43957  hoidmvle  44028  ovolval3  44075  ovolval4lem1  44077  smfpimbor1lem2  44220  gbpart7  45107  gbpart9  45109  gbpart11  45110  nnsum3primes4  45128  xpiun  45208  lindslinindsimp2lem5  45691  ackval42a  45931  aacllem  46391