Theorem eqtr2i 2761

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  3eqtrri  2765  3eqtr2ri  2767  dfun3  4217  dfif3  4482  dfsn2  4581  prprc1  4710  diftpsn3  4746  ssunpr  4778  sstp  4780  unidif0  5297  xpindi  5782  xpindir  5783  dmcnvcnv  5882  rncnvcnv  5883  imainrect  6139  dfrn4  6160  predres  6297  fcoi1  6708  foimacnv  6791  f1ossf1o  7075  fsnunfv  7135  difex2  7707  dfoprab3  8000  offval22  8031  suppvalbr  8107  fvmpocurryd  8214  mapsnconst  8833  sbthlem8  9025  fiint  9230  ordtypecbv  9425  trcl  9640  rankxplim2  9795  infdju1  10103  cfval2  10173  itunitc  10334  ituniiun  10335  hsmex2  10346  ltexnq  10889  ixi  11770  zeo  12606  num0h  12647  dec10p  12678  fseq1p1m1  13543  cats1fvn  14811  s3fn  14864  fsumrelem  15761  ef0lem  16034  ef01bndlem  16142  sadcadd  16418  sadadd2  16420  3lcm2e6woprm  16575  mod2xnegi  17033  str0  17150  ressinbas  17206  mreexexlem4d  17604  0g0  18623  frmdplusg  18813  smndex1bas  18868  sgrp2nmndlem4  18890  sgrp2nmndlem5  18891  oppgplusfval  19314  symgsubmefmnd  19364  psgnsn  19486  psgnprfval1  19488  frgpnabllem1  19839  opprmulfval  20310  opprrngb  20317  opprringb  20319  opprunit  20348  00lsp  20967  chrval  21513  dsmmelbas  21729  ltbwe  22032  ply1plusgfvi  22215  mat2pmatfval  22698  unisngl  23502  qtopres  23673  ufildr  23906  oppgtmd  24072  tgioo  24771  tgqioo  24775  dveflem  25956  lhop1lem  25990  sincos4thpi  26490  coskpi  26500  cxpsqrtlem  26679  log2ublem1  26923  efrlim  26946  efrlimOLD  26947  basellem3  27060  bposlem9  27269  madeun  27890  precsexlem11  28223  graop  29112  0grsubgr  29361  usgrfilem  29410  finsumvtxdg2ssteplem4  29632  wlkvtxedg  29727  2wlkdlem1  30008  2pthd  30023  wlk2v2e  30242  3wlkdlem1  30244  3pthd  30259  konigsberg  30342  cnidOLD  30668  ip1ilem  30912  ipasslem10  30925  normlem6  31201  dfhnorm2  31208  h1de2i  31639  spansnji  31732  pjneli  31809  mayetes3i  31815  pjclem1  32281  mdslmd3i  32418  atabsi  32487  imadifxp  32686  dfdec100  32918  sgnneg  32921  dpmul100  32971  dpmul1000  32973  dpmul4  32988  xrge00  33089  cyc2fv1  33197  cyc2fv2  33198  cyc3fv3  33215  opprlidlabs  33560  vieta  33739  cos9thpiminplylem5  33946  locfinref  34001  cnvordtrestixx  34073  raddcn  34089  rrhcn  34157  qqtopn  34171  esumpfinvallem  34234  sxbrsigalem1  34445  eulerpartgbij  34532  hgt750lem2  34812  subfacp1lem1  35377  subfacval2  35385  quad3  35868  ptrest  37954  poimirlem3  37958  poimirlem8  37963  poimirlem15  37970  mblfinlem3  37994  ismblfin  37996  areacirc  38048  pmapglb  40230  dvh4dimN  41907  hdmapfval  42287  12gcd5e1  42456  sqdeccom12  42735  remul02  42851  mapfzcons1  43163  lmhmlnmsplit  43533  pwssplit4  43535  clcnvlem  44068  cnvrcl0  44070  sqrtcval2  44087  resqrtvalex  44090  imsqrtvalex  44091  iunrelexp0  44147  sumnnodd  46078  climinf2mpt  46160  climinfmpt  46161  dvnmul  46389  wallispilem4  46514  dirkertrigeqlem3  46546  fourierdlem24  46577  fourierdlem57  46609  fourierdlem58  46610  fourierdlem80  46632  fourierswlem  46676  fouriersw  46677  fouriercn  46678  subsaliuncl  46804  gsumge0cl  46817  sge0tsms  46826  caragenuncllem  46958  0ome  46975  hoidmvle  47046  ovolval3  47093  ovolval4lem1  47095  smfpimbor1lem2  47245  gbpart7  48255  gbpart9  48257  gbpart11  48258  nnsum3primes4  48276  gpg5edgnedg  48618  xpiun  48646  lindslinindsimp2lem5  48950  ackval42a  49185  aacllem  50288