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  4230  dfif3  4496  dfsn2  4595  prprc1  4724  diftpsn3  4760  ssunpr  4792  sstp  4794  unidif0  5307  xpindi  5790  xpindir  5791  dmcnvcnv  5890  rncnvcnv  5891  imainrect  6147  dfrn4  6168  predres  6305  fcoi1  6716  foimacnv  6799  f1ossf1o  7083  fsnunfv  7143  difex2  7715  dfoprab3  8008  offval22  8040  suppvalbr  8116  fvmpocurryd  8223  mapsnconst  8842  sbthlem8  9034  fiint  9239  ordtypecbv  9434  trcl  9649  rankxplim2  9804  infdju1  10112  cfval2  10182  itunitc  10343  ituniiun  10344  hsmex2  10355  ltexnq  10898  ixi  11778  zeo  12590  num0h  12631  dec10p  12662  fseq1p1m1  13526  cats1fvn  14793  s3fn  14846  fsumrelem  15742  ef0lem  16013  ef01bndlem  16121  sadcadd  16397  sadadd2  16399  3lcm2e6woprm  16554  mod2xnegi  17011  str0  17128  ressinbas  17184  mreexexlem4d  17582  0g0  18601  frmdplusg  18791  smndex1bas  18843  sgrp2nmndlem4  18865  sgrp2nmndlem5  18866  oppgplusfval  19289  symgsubmefmnd  19339  psgnsn  19461  psgnprfval1  19463  frgpnabllem1  19814  opprmulfval  20287  opprrngb  20294  opprringb  20296  opprunit  20325  00lsp  20944  chrval  21490  dsmmelbas  21706  ltbwe  22011  ply1plusgfvi  22194  mat2pmatfval  22679  unisngl  23483  qtopres  23654  ufildr  23887  oppgtmd  24053  tgioo  24752  tgqioo  24756  dveflem  25951  lhop1lem  25986  sincos4thpi  26490  coskpi  26500  cxpsqrtlem  26679  log2ublem1  26924  efrlim  26947  efrlimOLD  26948  basellem3  27061  bposlem9  27271  madeun  27892  precsexlem11  28225  graop  29114  0grsubgr  29363  usgrfilem  29412  finsumvtxdg2ssteplem4  29634  wlkvtxedg  29729  2wlkdlem1  30010  2pthd  30025  wlk2v2e  30244  3wlkdlem1  30246  3pthd  30261  konigsberg  30344  cnidOLD  30670  ip1ilem  30914  ipasslem10  30927  normlem6  31203  dfhnorm2  31210  h1de2i  31641  spansnji  31734  pjneli  31811  mayetes3i  31817  pjclem1  32283  mdslmd3i  32420  atabsi  32489  imadifxp  32688  dfdec100  32922  sgnneg  32925  dpmul100  32989  dpmul1000  32991  dpmul4  33006  xrge00  33107  cyc2fv1  33215  cyc2fv2  33216  cyc3fv3  33233  opprlidlabs  33578  vieta  33757  cos9thpiminplylem5  33964  locfinref  34019  cnvordtrestixx  34091  raddcn  34107  rrhcn  34175  qqtopn  34189  esumpfinvallem  34252  sxbrsigalem1  34463  eulerpartgbij  34550  hgt750lem2  34830  subfacp1lem1  35395  subfacval2  35403  quad3  35886  ptrest  37870  poimirlem3  37874  poimirlem8  37879  poimirlem15  37886  mblfinlem3  37910  ismblfin  37912  areacirc  37964  pmapglb  40146  dvh4dimN  41823  hdmapfval  42203  12gcd5e1  42373  sqdeccom12  42659  remul02  42775  mapfzcons1  43074  lmhmlnmsplit  43444  pwssplit4  43446  clcnvlem  43979  cnvrcl0  43981  sqrtcval2  43998  resqrtvalex  44001  imsqrtvalex  44002  iunrelexp0  44058  sumnnodd  45990  climinf2mpt  46072  climinfmpt  46073  dvnmul  46301  wallispilem4  46426  dirkertrigeqlem3  46458  fourierdlem24  46489  fourierdlem57  46521  fourierdlem58  46522  fourierdlem80  46544  fourierswlem  46588  fouriersw  46589  fouriercn  46590  subsaliuncl  46716  gsumge0cl  46729  sge0tsms  46738  caragenuncllem  46870  0ome  46887  hoidmvle  46958  ovolval3  47005  ovolval4lem1  47007  smfpimbor1lem2  47157  gbpart7  48127  gbpart9  48129  gbpart11  48130  nnsum3primes4  48148  gpg5edgnedg  48490  xpiun  48518  lindslinindsimp2lem5  48822  ackval42a  49057  aacllem  50160