Theorem eqtr2i 2753

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 2752	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2738	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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  3eqtrri  2757  3eqtr2ri  2759  dfun3  4235  dfif3  4499  dfsn2  4598  prprc1  4725  diftpsn3  4762  ssunpr  4794  sstp  4796  unidif0  5310  xpindi  5787  xpindir  5788  dmcnvcnv  5886  rncnvcnv  5887  imainrect  6142  dfrn4  6163  predres  6300  fcoi1  6716  foimacnv  6799  f1ossf1o  7082  fsnunfv  7143  difex2  7716  dfoprab3  8012  offval22  8044  suppvalbr  8120  fvmpocurryd  8227  mapsnconst  8842  sbthlem8  9035  fiint  9253  fiintOLD  9254  ordtypecbv  9446  trcl  9657  rankxplim2  9809  infdju1  10119  cfval2  10189  itunitc  10350  ituniiun  10351  hsmex2  10362  ltexnq  10904  ixi  11783  zeo  12596  num0h  12637  dec10p  12668  fseq1p1m1  13535  cats1fvn  14800  s3fn  14853  fsumrelem  15749  ef0lem  16020  ef01bndlem  16128  sadcadd  16404  sadadd2  16406  3lcm2e6woprm  16561  mod2xnegi  17018  str0  17135  ressinbas  17191  mreexexlem4d  17584  0g0  18567  frmdplusg  18757  smndex1bas  18809  sgrp2nmndlem4  18831  sgrp2nmndlem5  18832  oppgplusfval  19256  symgsubmefmnd  19304  psgnsn  19426  psgnprfval1  19428  frgpnabllem1  19779  opprmulfval  20224  opprrngb  20231  opprringb  20233  opprunit  20262  00lsp  20863  chrval  21409  dsmmelbas  21624  ltbwe  21927  ply1plusgfvi  22102  mat2pmatfval  22586  unisngl  23390  qtopres  23561  ufildr  23794  oppgtmd  23960  tgioo  24660  tgqioo  24664  dveflem  25859  lhop1lem  25894  sincos4thpi  26398  coskpi  26408  cxpsqrtlem  26587  log2ublem1  26832  efrlim  26855  efrlimOLD  26856  basellem3  26969  bposlem9  27179  madeun  27771  precsexlem11  28095  0reno  28324  graop  28932  0grsubgr  29181  usgrfilem  29230  finsumvtxdg2ssteplem4  29452  wlkvtxedg  29547  2wlkdlem1  29828  2pthd  29843  wlk2v2e  30059  3wlkdlem1  30061  3pthd  30076  konigsberg  30159  cnidOLD  30484  ip1ilem  30728  ipasslem10  30741  normlem6  31017  dfhnorm2  31024  h1de2i  31455  spansnji  31548  pjneli  31625  mayetes3i  31631  pjclem1  32097  mdslmd3i  32234  atabsi  32303  imadifxp  32503  dfdec100  32728  sgnneg  32731  dpmul100  32790  dpmul1000  32792  dpmul4  32807  xrge00  32926  cyc2fv1  33051  cyc2fv2  33052  cyc3fv3  33069  opprlidlabs  33429  cos9thpiminplylem5  33749  locfinref  33804  cnvordtrestixx  33876  raddcn  33892  rrhcn  33960  qqtopn  33974  esumpfinvallem  34037  sxbrsigalem1  34249  eulerpartgbij  34336  hgt750lem2  34616  subfacp1lem1  35139  subfacval2  35147  quad3  35630  ptrest  37586  poimirlem3  37590  poimirlem8  37595  poimirlem15  37602  mblfinlem3  37626  ismblfin  37628  areacirc  37680  pmapglb  39737  dvh4dimN  41414  hdmapfval  41794  12gcd5e1  41964  sqdeccom12  42250  remul02  42366  mapfzcons1  42678  lmhmlnmsplit  43049  pwssplit4  43051  clcnvlem  43585  cnvrcl0  43587  sqrtcval2  43604  resqrtvalex  43607  imsqrtvalex  43608  iunrelexp0  43664  sumnnodd  45601  climinf2mpt  45685  climinfmpt  45686  dvnmul  45914  wallispilem4  46039  dirkertrigeqlem3  46071  fourierdlem24  46102  fourierdlem57  46134  fourierdlem58  46135  fourierdlem80  46157  fourierswlem  46201  fouriersw  46202  fouriercn  46203  subsaliuncl  46329  gsumge0cl  46342  sge0tsms  46351  caragenuncllem  46483  0ome  46500  hoidmvle  46571  ovolval3  46618  ovolval4lem1  46620  smfpimbor1lem2  46770  gbpart7  47741  gbpart9  47743  gbpart11  47744  nnsum3primes4  47762  xpiun  48119  lindslinindsimp2lem5  48424  ackval42a  48659  aacllem  49763