Theorem eqtr2i 2847

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  3eqtrri  2851  3eqtr2ri  2853  dfun3  4244  dfif3  4483  dfsn2  4582  prprc1  4703  diftpsn3  4737  ssunpr  4767  sstp  4769  unidif0  5262  pwundifOLD  5459  xpindi  5706  xpindir  5707  dmcnvcnv  5805  rncnvcnv  5806  imainrect  6040  dfrn4  6061  fcoi1  6554  foimacnv  6634  f1ossf1o  6892  fsnunfv  6951  difex2  7484  dfoprab3  7754  offval22  7785  fvmpocurryd  7939  mapsnconst  8458  sbthlem8  8636  fiint  8797  ordtypecbv  8983  ruv  9068  trcl  9172  rankxplim2  9311  infdju1  9617  cfval2  9684  itunitc  9845  ituniiun  9846  hsmex2  9857  ltexnq  10399  ixi  11271  zeo  12071  num0h  12113  dec10p  12144  fseq1p1m1  12984  cats1fvn  14222  s3fn  14275  fsumrelem  15164  ef0lem  15434  ef01bndlem  15539  sadcadd  15809  sadadd2  15811  3lcm2e6woprm  15961  mod2xnegi  16409  decexp2  16413  str0  16537  ressinbas  16562  mreexexlem4d  16920  0g0  17876  frmdplusg  18021  smndex1bas  18073  sgrp2nmndlem4  18095  sgrp2nmndlem5  18096  oppgplusfval  18478  symgsubmefmnd  18528  psgnsn  18650  psgnprfval1  18652  frgpnabllem1  18995  opprmulfval  19377  opprringb  19384  opprunit  19413  00lsp  19755  ltbwe  20255  ply1plusgfvi  20412  chrval  20674  dsmmelbas  20885  mat2pmatfval  21333  unisngl  22137  qtopres  22308  ufildr  22541  oppgtmd  22707  tgioo  23406  tgqioo  23410  dveflem  24578  lhop1lem  24612  sincos4thpi  25101  coskpi  25110  cxpsqrtlem  25287  log2ublem1  25526  efrlim  25549  basellem3  25662  bposlem9  25870  graop  26816  0grsubgr  27062  usgrfilem  27111  finsumvtxdg2ssteplem4  27332  wlkvtxedg  27427  2wlkdlem1  27706  2pthd  27721  wlk2v2e  27938  3wlkdlem1  27940  3pthd  27955  konigsberg  28038  cnidOLD  28361  ip1ilem  28605  ipasslem10  28618  normlem6  28894  dfhnorm2  28901  h1de2i  29332  spansnji  29425  pjneli  29502  mayetes3i  29508  pjclem1  29974  mdslmd3i  30111  atabsi  30180  imadifxp  30353  dfdec100  30548  dpmul100  30575  dpmul1000  30577  dpmul4  30592  xrge00  30675  cyc2fv1  30765  cyc2fv2  30766  cyc3fv3  30783  locfinref  31107  cnvordtrestixx  31158  raddcn  31174  rrhcn  31240  qqtopn  31254  esumpfinvallem  31335  sxbrsigalem1  31545  eulerpartgbij  31632  sgnneg  31800  hgt750lem2  31925  subfacp1lem1  32428  subfacval2  32436  quad3  32915  ptrest  34893  poimirlem3  34897  poimirlem8  34902  poimirlem15  34909  mblfinlem3  34933  ismblfin  34935  areacirc  34989  pmapglb  36908  dvh4dimN  38585  hdmapfval  38965  sqdeccom12  39182  remul02  39242  mapfzcons1  39321  lmhmlnmsplit  39694  pwssplit4  39696  clcnvlem  39990  cnvrcl0  39992  iunrelexp0  40054  sumnnodd  41918  climinf2mpt  42002  climinfmpt  42003  dvnmul  42235  wallispilem4  42360  dirkertrigeqlem3  42392  fourierdlem24  42423  fourierdlem57  42455  fourierdlem58  42456  fourierdlem80  42478  fourierswlem  42522  fouriersw  42523  fouriercn  42524  subsaliuncl  42648  gsumge0cl  42660  sge0tsms  42669  caragenuncllem  42801  0ome  42818  hoidmvle  42889  ovolval3  42936  ovolval4lem1  42938  smfpimbor1lem2  43081  gbpart7  43939  gbpart9  43941  gbpart11  43942  nnsum3primes4  43960  xpiun  44040  lindslinindsimp2lem5  44524  aacllem  44909