Theorem eqtr2i 2755

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

Syntax hints:   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  3eqtrri  2759  3eqtr2ri  2761  dfun3  4267  dfif3  4547  dfsn2  4646  prprc1  4774  diftpsn3  4811  ssunpr  4841  sstp  4843  unidif0  5364  xpindi  5840  xpindir  5841  dmcnvcnv  5939  rncnvcnv  5940  imainrect  6192  dfrn4  6213  predres  6352  fcoi1  6776  foimacnv  6860  f1ossf1o  7142  fsnunfv  7201  difex2  7768  dfoprab3  8068  offval22  8102  suppvalbr  8178  fvmpocurryd  8286  mapsnconst  8921  sbthlem8  9128  fiint  9368  fiintOLD  9369  ordtypecbv  9560  trcl  9771  rankxplim2  9923  infdju1  10232  cfval2  10303  itunitc  10464  ituniiun  10465  hsmex2  10476  ltexnq  11018  ixi  11893  zeo  12700  num0h  12741  dec10p  12772  fseq1p1m1  13629  cats1fvn  14867  s3fn  14920  fsumrelem  15811  ef0lem  16080  ef01bndlem  16186  sadcadd  16458  sadadd2  16460  3lcm2e6woprm  16616  mod2xnegi  17073  decexp2  17077  str0  17191  ressinbas  17259  mreexexlem4d  17660  0g0  18657  frmdplusg  18844  smndex1bas  18896  sgrp2nmndlem4  18918  sgrp2nmndlem5  18919  oppgplusfval  19342  symgsubmefmnd  19396  psgnsn  19518  psgnprfval1  19520  frgpnabllem1  19871  opprmulfval  20318  opprrngb  20328  opprringb  20330  opprunit  20359  00lsp  20958  chrval  21517  dsmmelbas  21737  ltbwe  22051  ply1plusgfvi  22231  mat2pmatfval  22716  unisngl  23522  qtopres  23693  ufildr  23926  oppgtmd  24092  tgioo  24803  tgqioo  24807  dveflem  26002  lhop1lem  26037  sincos4thpi  26541  coskpi  26550  cxpsqrtlem  26729  log2ublem1  26974  efrlim  26997  efrlimOLD  26998  basellem3  27111  bposlem9  27321  madeun  27907  precsexlem11  28216  0reno  28348  graop  28965  0grsubgr  29214  usgrfilem  29263  finsumvtxdg2ssteplem4  29485  wlkvtxedg  29581  2wlkdlem1  29859  2pthd  29874  wlk2v2e  30090  3wlkdlem1  30092  3pthd  30107  konigsberg  30190  cnidOLD  30515  ip1ilem  30759  ipasslem10  30772  normlem6  31048  dfhnorm2  31055  h1de2i  31486  spansnji  31579  pjneli  31656  mayetes3i  31662  pjclem1  32128  mdslmd3i  32265  atabsi  32334  imadifxp  32521  dfdec100  32731  dpmul100  32758  dpmul1000  32760  dpmul4  32775  xrge00  32895  cyc2fv1  32999  cyc2fv2  33000  cyc3fv3  33017  opprlidlabs  33360  locfinref  33656  cnvordtrestixx  33728  raddcn  33744  rrhcn  33812  qqtopn  33826  esumpfinvallem  33907  sxbrsigalem1  34119  eulerpartgbij  34206  sgnneg  34374  hgt750lem2  34498  subfacp1lem1  35007  subfacval2  35015  quad3  35498  ptrest  37320  poimirlem3  37324  poimirlem8  37329  poimirlem15  37336  mblfinlem3  37360  ismblfin  37362  areacirc  37414  pmapglb  39469  dvh4dimN  41146  hdmapfval  41526  12gcd5e1  41702  sqdeccom12  42102  remul02  42185  mapfzcons1  42374  lmhmlnmsplit  42748  pwssplit4  42750  clcnvlem  43290  cnvrcl0  43292  sqrtcval2  43309  resqrtvalex  43312  imsqrtvalex  43313  iunrelexp0  43369  sumnnodd  45251  climinf2mpt  45335  climinfmpt  45336  dvnmul  45564  wallispilem4  45689  dirkertrigeqlem3  45721  fourierdlem24  45752  fourierdlem57  45784  fourierdlem58  45785  fourierdlem80  45807  fourierswlem  45851  fouriersw  45852  fouriercn  45853  subsaliuncl  45979  gsumge0cl  45992  sge0tsms  46001  caragenuncllem  46133  0ome  46150  hoidmvle  46221  ovolval3  46268  ovolval4lem1  46270  smfpimbor1lem2  46420  gbpart7  47339  gbpart9  47341  gbpart11  47342  nnsum3primes4  47360  xpiun  47535  lindslinindsimp2lem5  47845  ackval42a  48085  aacllem  48549