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  4748  ssunpr  4778  sstp  4780  unidif0OLD  5303  xpindi  5789  xpindir  5790  dmcnvcnv  5889  rncnvcnv  5890  imainrect  6146  dfrn4  6167  predres  6304  fcoi1  6715  foimacnv  6798  f1ossf1o  7082  fsnunfv  7142  difex2  7714  dfoprab3  8007  offval22  8038  suppvalbr  8114  fvmpocurryd  8221  mapsnconst  8840  sbthlem8  9032  fiint  9237  ordtypecbv  9432  trcl  9649  rankxplim2  9804  infdju1  10112  cfval2  10182  itunitc  10343  ituniiun  10344  hsmex2  10355  ltexnq  10898  ixi  11779  zeo  12615  num0h  12656  dec10p  12687  fseq1p1m1  13552  cats1fvn  14820  s3fn  14873  fsumrelem  15770  ef0lem  16043  ef01bndlem  16151  sadcadd  16427  sadadd2  16429  3lcm2e6woprm  16584  mod2xnegi  17042  str0  17159  ressinbas  17215  mreexexlem4d  17613  0g0  18632  frmdplusg  18822  smndex1bas  18877  sgrp2nmndlem4  18899  sgrp2nmndlem5  18900  oppgplusfval  19323  symgsubmefmnd  19373  psgnsn  19495  psgnprfval1  19497  frgpnabllem1  19848  opprmulfval  20319  opprrngb  20326  opprringb  20328  opprunit  20357  00lsp  20976  chrval  21503  dsmmelbas  21719  ltbwe  22022  ply1plusgfvi  22205  mat2pmatfval  22688  unisngl  23492  qtopres  23663  ufildr  23896  oppgtmd  24062  tgioo  24761  tgqioo  24765  dveflem  25946  lhop1lem  25980  sincos4thpi  26477  coskpi  26487  cxpsqrtlem  26666  log2ublem1  26910  efrlim  26933  basellem3  27046  bposlem9  27255  madeun  27876  precsexlem11  28209  graop  29098  0grsubgr  29347  usgrfilem  29396  finsumvtxdg2ssteplem4  29617  wlkvtxedg  29712  2wlkdlem1  29993  2pthd  30008  wlk2v2e  30227  3wlkdlem1  30229  3pthd  30244  konigsberg  30327  cnidOLD  30653  ip1ilem  30897  ipasslem10  30910  normlem6  31186  dfhnorm2  31193  h1de2i  31624  spansnji  31717  pjneli  31794  mayetes3i  31800  pjclem1  32266  mdslmd3i  32403  atabsi  32472  imadifxp  32671  dfdec100  32903  sgnneg  32906  dpmul100  32956  dpmul1000  32958  dpmul4  32973  xrge00  33074  cyc2fv1  33182  cyc2fv2  33183  cyc3fv3  33200  opprlidlabs  33545  vieta  33724  cos9thpiminplylem5  33930  locfinref  33985  cnvordtrestixx  34057  raddcn  34073  rrhcn  34141  qqtopn  34155  esumpfinvallem  34218  sxbrsigalem1  34429  eulerpartgbij  34516  hgt750lem2  34796  subfacp1lem1  35361  subfacval2  35369  quad3  35852  ptrest  37940  poimirlem3  37944  poimirlem8  37949  poimirlem15  37956  mblfinlem3  37980  ismblfin  37982  areacirc  38034  pmapglb  40216  dvh4dimN  41893  hdmapfval  42273  12gcd5e1  42442  sqdeccom12  42721  remul02  42837  mapfzcons1  43149  lmhmlnmsplit  43515  pwssplit4  43517  clcnvlem  44050  cnvrcl0  44052  sqrtcval2  44069  resqrtvalex  44072  imsqrtvalex  44073  iunrelexp0  44129  sumnnodd  46060  climinf2mpt  46142  climinfmpt  46143  dvnmul  46371  wallispilem4  46496  dirkertrigeqlem3  46528  fourierdlem24  46559  fourierdlem57  46591  fourierdlem58  46592  fourierdlem80  46614  fourierswlem  46658  fouriersw  46659  fouriercn  46660  subsaliuncl  46786  gsumge0cl  46799  sge0tsms  46808  caragenuncllem  46940  0ome  46957  hoidmvle  47028  ovolval3  47075  ovolval4lem1  47077  smfpimbor1lem2  47227  gbpart7  48237  gbpart9  48239  gbpart11  48240  nnsum3primes4  48258  gpg5edgnedg  48600  xpiun  48628  lindslinindsimp2lem5  48932  ackval42a  49167  aacllem  50270