Theorem eqtr2i 2845

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  3eqtrri  2849  3eqtr2ri  2851  dfun3  4242  dfif3  4481  dfsn2  4574  prprc1  4695  diftpsn3  4729  ssunpr  4759  sstp  4761  unidif0  5253  pwundifOLD  5452  xpindi  5699  xpindir  5700  dmcnvcnv  5798  rncnvcnv  5799  imainrect  6033  dfrn4  6054  fcoi1  6547  foimacnv  6627  f1ossf1o  6885  fsnunfv  6944  difex2  7476  dfoprab3  7746  offval22  7777  fvmpocurryd  7931  mapsnconst  8450  sbthlem8  8628  fiint  8789  ordtypecbv  8975  ruv  9060  trcl  9164  rankxplim2  9303  infdju1  9609  cfval2  9676  itunitc  9837  ituniiun  9838  hsmex2  9849  ltexnq  10391  ixi  11263  zeo  12062  num0h  12104  dec10p  12135  fseq1p1m1  12975  cats1fvn  14214  s3fn  14267  fsumrelem  15156  ef0lem  15426  ef01bndlem  15531  sadcadd  15801  sadadd2  15803  3lcm2e6woprm  15953  mod2xnegi  16401  decexp2  16405  str0  16529  ressinbas  16554  mreexexlem4d  16912  0g0  17868  frmdplusg  18013  smndex1bas  18065  sgrp2nmndlem4  18087  sgrp2nmndlem5  18088  oppgplusfval  18470  symgsubmefmnd  18520  psgnsn  18642  psgnprfval1  18644  frgpnabllem1  18987  opprmulfval  19369  opprringb  19376  opprunit  19405  00lsp  19747  ltbwe  20247  ply1plusgfvi  20404  chrval  20666  dsmmelbas  20877  mat2pmatfval  21325  unisngl  22129  qtopres  22300  ufildr  22533  oppgtmd  22699  tgioo  23398  tgqioo  23402  dveflem  24570  lhop1lem  24604  sincos4thpi  25093  coskpi  25102  cxpsqrtlem  25279  log2ublem1  25518  efrlim  25541  basellem3  25654  bposlem9  25862  graop  26808  0grsubgr  27054  usgrfilem  27103  finsumvtxdg2ssteplem4  27324  wlkvtxedg  27419  2wlkdlem1  27698  2pthd  27713  wlk2v2e  27930  3wlkdlem1  27932  3pthd  27947  konigsberg  28030  cnidOLD  28353  ip1ilem  28597  ipasslem10  28610  normlem6  28886  dfhnorm2  28893  h1de2i  29324  spansnji  29417  pjneli  29494  mayetes3i  29500  pjclem1  29966  mdslmd3i  30103  atabsi  30172  imadifxp  30345  dfdec100  30541  dpmul100  30568  dpmul1000  30570  dpmul4  30585  xrge00  30668  cyc2fv1  30758  cyc2fv2  30759  cyc3fv3  30776  locfinref  31100  cnvordtrestixx  31151  raddcn  31167  rrhcn  31233  qqtopn  31247  esumpfinvallem  31328  sxbrsigalem1  31538  eulerpartgbij  31625  sgnneg  31793  hgt750lem2  31918  subfacp1lem1  32421  subfacval2  32429  quad3  32908  ptrest  34885  poimirlem3  34889  poimirlem8  34894  poimirlem15  34901  mblfinlem3  34925  ismblfin  34927  areacirc  34981  pmapglb  36900  dvh4dimN  38577  hdmapfval  38957  sqdeccom12  39168  remul02  39228  mapfzcons1  39307  lmhmlnmsplit  39680  pwssplit4  39682  clcnvlem  39976  cnvrcl0  39978  iunrelexp0  40040  sumnnodd  41903  climinf2mpt  41987  climinfmpt  41988  dvnmul  42220  wallispilem4  42346  dirkertrigeqlem3  42378  fourierdlem24  42409  fourierdlem57  42441  fourierdlem58  42442  fourierdlem80  42464  fourierswlem  42508  fouriersw  42509  fouriercn  42510  subsaliuncl  42634  gsumge0cl  42646  sge0tsms  42655  caragenuncllem  42787  0ome  42804  hoidmvle  42875  ovolval3  42922  ovolval4lem1  42924  smfpimbor1lem2  43067  gbpart7  43925  gbpart9  43927  gbpart11  43928  nnsum3primes4  43946  xpiun  44026  lindslinindsimp2lem5  44510  aacllem  44895