Theorem eqtr2i 2822

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

Syntax hints:   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  3eqtrri  2826  3eqtr2ri  2828  dfun3  4192  dfif3  4439  dfsn2  4538  prprc1  4661  diftpsn3  4695  ssunpr  4725  sstp  4727  unidif0  5225  pwundifOLD  5422  xpindi  5668  xpindir  5669  dmcnvcnv  5767  rncnvcnv  5768  imainrect  6005  dfrn4  6026  fcoi1  6526  foimacnv  6607  f1ossf1o  6867  fsnunfv  6926  difex2  7462  dfoprab3  7734  offval22  7766  fvmpocurryd  7920  mapsnconst  8439  sbthlem8  8618  fiint  8779  ordtypecbv  8965  ruv  9050  trcl  9154  rankxplim2  9293  infdju1  9600  cfval2  9671  itunitc  9832  ituniiun  9833  hsmex2  9844  ltexnq  10386  ixi  11258  zeo  12056  num0h  12098  dec10p  12129  fseq1p1m1  12976  cats1fvn  14211  s3fn  14264  fsumrelem  15154  ef0lem  15424  ef01bndlem  15529  sadcadd  15797  sadadd2  15799  3lcm2e6woprm  15949  mod2xnegi  16397  decexp2  16401  str0  16527  ressinbas  16552  mreexexlem4d  16910  0g0  17866  frmdplusg  18011  smndex1bas  18063  sgrp2nmndlem4  18085  sgrp2nmndlem5  18086  oppgplusfval  18468  symgsubmefmnd  18518  psgnsn  18640  psgnprfval1  18642  frgpnabllem1  18986  opprmulfval  19371  opprringb  19378  opprunit  19407  00lsp  19746  chrval  20217  dsmmelbas  20428  ltbwe  20712  ply1plusgfvi  20871  mat2pmatfval  21328  unisngl  22132  qtopres  22303  ufildr  22536  oppgtmd  22702  tgioo  23401  tgqioo  23405  dveflem  24582  lhop1lem  24616  sincos4thpi  25106  coskpi  25115  cxpsqrtlem  25293  log2ublem1  25532  efrlim  25555  basellem3  25668  bposlem9  25876  graop  26822  0grsubgr  27068  usgrfilem  27117  finsumvtxdg2ssteplem4  27338  wlkvtxedg  27433  2wlkdlem1  27711  2pthd  27726  wlk2v2e  27942  3wlkdlem1  27944  3pthd  27959  konigsberg  28042  cnidOLD  28365  ip1ilem  28609  ipasslem10  28622  normlem6  28898  dfhnorm2  28905  h1de2i  29336  spansnji  29429  pjneli  29506  mayetes3i  29512  pjclem1  29978  mdslmd3i  30115  atabsi  30184  imadifxp  30364  dfdec100  30572  dpmul100  30599  dpmul1000  30601  dpmul4  30616  xrge00  30720  cyc2fv1  30813  cyc2fv2  30814  cyc3fv3  30831  locfinref  31194  cnvordtrestixx  31266  raddcn  31282  rrhcn  31348  qqtopn  31362  esumpfinvallem  31443  sxbrsigalem1  31653  eulerpartgbij  31740  sgnneg  31908  hgt750lem2  32033  subfacp1lem1  32539  subfacval2  32547  quad3  33026  ptrest  35056  poimirlem3  35060  poimirlem8  35065  poimirlem15  35072  mblfinlem3  35096  ismblfin  35098  areacirc  35150  pmapglb  37066  dvh4dimN  38743  hdmapfval  39123  12gcd5e1  39291  3lexlogpow5ineq1  39341  sqdeccom12  39483  remul02  39543  mapfzcons1  39658  lmhmlnmsplit  40031  pwssplit4  40033  clcnvlem  40323  cnvrcl0  40325  sqrtcval2  40342  resqrtvalex  40345  imsqrtvalex  40346  iunrelexp0  40403  sumnnodd  42272  climinf2mpt  42356  climinfmpt  42357  dvnmul  42585  wallispilem4  42710  dirkertrigeqlem3  42742  fourierdlem24  42773  fourierdlem57  42805  fourierdlem58  42806  fourierdlem80  42828  fourierswlem  42872  fouriersw  42873  fouriercn  42874  subsaliuncl  42998  gsumge0cl  43010  sge0tsms  43019  caragenuncllem  43151  0ome  43168  hoidmvle  43239  ovolval3  43286  ovolval4lem1  43288  smfpimbor1lem2  43431  gbpart7  44285  gbpart9  44287  gbpart11  44288  nnsum3primes4  44306  xpiun  44386  lindslinindsimp2lem5  44871  ackval42a  45111  aacllem  45329