Theorem eqtr2i 2766

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 2765	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2746	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3eqtrri  2770  3eqtr2ri  2772  dfun3  4276  dfif3  4540  dfsn2  4639  prprc1  4765  diftpsn3  4802  ssunpr  4834  sstp  4836  unidif0  5360  xpindi  5844  xpindir  5845  dmcnvcnv  5944  rncnvcnv  5945  imainrect  6201  dfrn4  6222  predres  6360  fcoi1  6782  foimacnv  6865  f1ossf1o  7148  fsnunfv  7207  difex2  7780  dfoprab3  8079  offval22  8113  suppvalbr  8189  fvmpocurryd  8296  mapsnconst  8932  sbthlem8  9130  fiint  9366  fiintOLD  9367  ordtypecbv  9557  trcl  9768  rankxplim2  9920  infdju1  10230  cfval2  10300  itunitc  10461  ituniiun  10462  hsmex2  10473  ltexnq  11015  ixi  11892  zeo  12704  num0h  12745  dec10p  12776  fseq1p1m1  13638  cats1fvn  14897  s3fn  14950  fsumrelem  15843  ef0lem  16114  ef01bndlem  16220  sadcadd  16495  sadadd2  16497  3lcm2e6woprm  16652  mod2xnegi  17109  str0  17226  ressinbas  17291  mreexexlem4d  17690  0g0  18677  frmdplusg  18867  smndex1bas  18919  sgrp2nmndlem4  18941  sgrp2nmndlem5  18942  oppgplusfval  19366  symgsubmefmnd  19416  psgnsn  19538  psgnprfval1  19540  frgpnabllem1  19891  opprmulfval  20336  opprrngb  20346  opprringb  20348  opprunit  20377  00lsp  20979  chrval  21538  dsmmelbas  21759  ltbwe  22062  ply1plusgfvi  22243  mat2pmatfval  22729  unisngl  23535  qtopres  23706  ufildr  23939  oppgtmd  24105  tgioo  24817  tgqioo  24821  dveflem  26017  lhop1lem  26052  sincos4thpi  26555  coskpi  26565  cxpsqrtlem  26744  log2ublem1  26989  efrlim  27012  efrlimOLD  27013  basellem3  27126  bposlem9  27336  madeun  27922  precsexlem11  28241  0reno  28429  graop  29046  0grsubgr  29295  usgrfilem  29344  finsumvtxdg2ssteplem4  29566  wlkvtxedg  29662  2wlkdlem1  29945  2pthd  29960  wlk2v2e  30176  3wlkdlem1  30178  3pthd  30193  konigsberg  30276  cnidOLD  30601  ip1ilem  30845  ipasslem10  30858  normlem6  31134  dfhnorm2  31141  h1de2i  31572  spansnji  31665  pjneli  31742  mayetes3i  31748  pjclem1  32214  mdslmd3i  32351  atabsi  32420  imadifxp  32614  dfdec100  32832  dpmul100  32879  dpmul1000  32881  dpmul4  32896  xrge00  33017  cyc2fv1  33141  cyc2fv2  33142  cyc3fv3  33159  opprlidlabs  33513  locfinref  33840  cnvordtrestixx  33912  raddcn  33928  rrhcn  33998  qqtopn  34012  esumpfinvallem  34075  sxbrsigalem1  34287  eulerpartgbij  34374  sgnneg  34543  hgt750lem2  34667  subfacp1lem1  35184  subfacval2  35192  quad3  35675  ptrest  37626  poimirlem3  37630  poimirlem8  37635  poimirlem15  37642  mblfinlem3  37666  ismblfin  37668  areacirc  37720  pmapglb  39772  dvh4dimN  41449  hdmapfval  41829  12gcd5e1  42004  sqdeccom12  42324  remul02  42435  mapfzcons1  42728  lmhmlnmsplit  43099  pwssplit4  43101  clcnvlem  43636  cnvrcl0  43638  sqrtcval2  43655  resqrtvalex  43658  imsqrtvalex  43659  iunrelexp0  43715  sumnnodd  45645  climinf2mpt  45729  climinfmpt  45730  dvnmul  45958  wallispilem4  46083  dirkertrigeqlem3  46115  fourierdlem24  46146  fourierdlem57  46178  fourierdlem58  46179  fourierdlem80  46201  fourierswlem  46245  fouriersw  46246  fouriercn  46247  subsaliuncl  46373  gsumge0cl  46386  sge0tsms  46395  caragenuncllem  46527  0ome  46544  hoidmvle  46615  ovolval3  46662  ovolval4lem1  46664  smfpimbor1lem2  46814  gbpart7  47754  gbpart9  47756  gbpart11  47757  nnsum3primes4  47775  xpiun  48074  lindslinindsimp2lem5  48379  ackval42a  48618  aacllem  49320