Theorem eqtr2i 2645

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)

Hypotheses

Ref	Expression
eqtr2i.1	|- A = B
eqtr2i.2	|- B = C

Assertion

Ref	Expression
eqtr2i	|- C = A

Proof of Theorem eqtr2i

Step	Hyp	Ref	Expression
1		eqtr2i.1	. . 3 |- A = B
2		eqtr2i.2	. . 3 |- B = C
3	1, 2	eqtri 2644	. 2 |- A = C
4	3	eqcomi 2631	1 |- C = A

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  3eqtrri  2649  3eqtr2ri  2651  dfun3  3865  dfif3  4100  dfsn2  4190  prprc1  4300  diftpsn3  4332  ssunpr  4365  sstp  4367  unidif0  4838  pwundif  5021  xpindi  5255  xpindir  5256  dmcnvcnv  5348  rncnvcnv  5349  imainrect  5575  dfrn4  5595  fcoi1  6078  foimacnv  6154  fsnunfv  6453  difex2  6969  dfoprab3  7224  offval22  7253  fvmpt2curryd  7397  mapsnconst  7903  sbthlem8  8077  fiint  8237  ordtypecbv  8422  ruv  8507  trcl  8604  rankxplim2  8743  infcda1  9015  cfval2  9082  itunitc  9243  ituniiun  9244  hsmex2  9255  ltexnq  9797  ixi  10656  zeo  11463  num0h  11509  dec10p  11553  dec10pOLD  11554  fseq1p1m1  12414  cats1fvn  13603  s3fn  13656  fsumrelem  14539  ef0lem  14809  ef01bndlem  14914  sadcadd  15180  sadadd2  15182  3lcm2e6woprm  15328  mod2xnegi  15775  decexp2  15779  str0  15911  ressinbas  15936  mreexexlem4d  16307  0g0  17263  frmdplusg  17391  sgrp2nmndlem4  17415  sgrp2nmndlem5  17416  oppgplusfval  17778  psgnsn  17940  psgnprfval1  17942  frgpnabllem1  18276  opprmulfval  18625  opprringb  18632  opprunit  18661  00lsp  18981  psrmulr  19384  ltbwe  19472  ply1plusgfvi  19612  chrval  19873  dsmmelbas  20083  mat2pmatfval  20528  unisngl  21330  qtopres  21501  ufildr  21735  oppgtmd  21901  tgioo  22599  tgqioo  22603  dveflem  23742  lhop1lem  23776  sincos4thpi  24265  coskpi  24272  cxpsqrtlem  24448  log2ublem1  24673  efrlim  24696  basellem3  24809  bposlem9  25017  graop  25921  0grsubgr  26170  usgrfilem  26219  finsumvtxdg2ssteplem4  26444  wlkvtxedg  26540  2wlkdlem1  26821  2pthd  26836  wlk2v2e  27017  3wlkdlem1  27019  3pthd  27034  konigsberg  27119  cnidOLD  27437  ip1ilem  27681  ipasslem10  27694  normlem6  27972  dfhnorm2  27979  h1de2i  28412  spansnji  28505  pjneli  28582  mayetes3i  28588  pjclem1  29054  mdslmd3i  29191  atabsi  29260  imadifxp  29414  dfdec100  29576  dpmul100  29605  dpmul1000  29607  dpmul4  29622  xrge00  29686  locfinref  29908  cnvordtrestixx  29959  raddcn  29975  rrhcn  30041  qqtopn  30055  esumpfinvallem  30136  isrnsigaOLD  30175  sxbrsigalem1  30347  eulerpartgbij  30434  sgnneg  30602  hgt750lem2  30730  subfacp1lem1  31161  subfacval2  31169  quad3  31564  ptrest  33408  poimirlem3  33412  poimirlem8  33417  poimirlem15  33424  mblfinlem3  33448  ismblfin  33450  areacirc  33505  pmapglb  35056  dvh4dimN  36736  hdmapfval  37119  mapfzcons1  37280  lmhmlnmsplit  37657  pwssplit4  37659  clcnvlem  37930  cnvrcl0  37932  iunrelexp0  37994  sumnnodd  39862  climinf2mpt  39946  climinfmpt  39947  dvnmul  40158  wallispilem4  40285  dirkertrigeqlem3  40317  fourierdlem24  40348  fourierdlem57  40380  fourierdlem58  40381  fourierdlem80  40403  fourierswlem  40447  fouriersw  40448  fouriercn  40449  subsaliuncl  40576  gsumge0cl  40588  sge0tsms  40597  caragenuncllem  40726  0ome  40743  hoidmvle  40814  ovolval3  40861  ovolval4lem1  40863  smfpimbor1lem2  41006  gbpart7  41655  gbpart9  41657  gbpart11  41658  nnsum3primes4  41676  xpiun  41766  lindslinindsimp2lem5  42251  aacllem  42547