Theorem eqtr2i 2760

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 2759	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2745	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 2708

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

This theorem is referenced by:  3eqtrri  2764  3eqtr2ri  2766  dfun3  4216  dfif3  4481  dfsn2  4580  prprc1  4709  diftpsn3  4747  ssunpr  4777  sstp  4779  unidif0OLD  5302  xpindi  5788  xpindir  5789  dmcnvcnv  5888  rncnvcnv  5889  imainrect  6145  dfrn4  6166  predres  6303  fcoi1  6714  foimacnv  6797  f1ossf1o  7081  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  48243  gbpart9  48245  gbpart11  48246  nnsum3primes4  48264  gpg5edgnedg  48606  xpiun  48634  lindslinindsimp2lem5  48938  ackval42a  49173  aacllem  50276