Theorem eqtr2i 2763

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

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  3eqtrri  2767  3eqtr2ri  2769  dfun3  4281  dfif3  4544  dfsn2  4643  prprc1  4769  diftpsn3  4806  ssunpr  4838  sstp  4840  unidif0  5365  xpindi  5846  xpindir  5847  dmcnvcnv  5946  rncnvcnv  5947  imainrect  6202  dfrn4  6223  predres  6361  fcoi1  6782  foimacnv  6865  f1ossf1o  7147  fsnunfv  7206  difex2  7778  dfoprab3  8077  offval22  8111  suppvalbr  8187  fvmpocurryd  8294  mapsnconst  8930  sbthlem8  9128  fiint  9363  fiintOLD  9364  ordtypecbv  9554  trcl  9765  rankxplim2  9917  infdju1  10227  cfval2  10297  itunitc  10458  ituniiun  10459  hsmex2  10470  ltexnq  11012  ixi  11889  zeo  12701  num0h  12742  dec10p  12773  fseq1p1m1  13634  cats1fvn  14893  s3fn  14946  fsumrelem  15839  ef0lem  16110  ef01bndlem  16216  sadcadd  16491  sadadd2  16493  3lcm2e6woprm  16648  mod2xnegi  17104  decexp2  17108  str0  17222  ressinbas  17290  mreexexlem4d  17691  0g0  18689  frmdplusg  18879  smndex1bas  18931  sgrp2nmndlem4  18953  sgrp2nmndlem5  18954  oppgplusfval  19378  symgsubmefmnd  19430  psgnsn  19552  psgnprfval1  19554  frgpnabllem1  19905  opprmulfval  20352  opprrngb  20362  opprringb  20364  opprunit  20393  00lsp  20996  chrval  21555  dsmmelbas  21776  ltbwe  22079  ply1plusgfvi  22258  mat2pmatfval  22744  unisngl  23550  qtopres  23721  ufildr  23954  oppgtmd  24120  tgioo  24831  tgqioo  24835  dveflem  26031  lhop1lem  26066  sincos4thpi  26569  coskpi  26579  cxpsqrtlem  26758  log2ublem1  27003  efrlim  27026  efrlimOLD  27027  basellem3  27140  bposlem9  27350  madeun  27936  precsexlem11  28255  0reno  28443  graop  29060  0grsubgr  29309  usgrfilem  29358  finsumvtxdg2ssteplem4  29580  wlkvtxedg  29676  2wlkdlem1  29954  2pthd  29969  wlk2v2e  30185  3wlkdlem1  30187  3pthd  30202  konigsberg  30285  cnidOLD  30610  ip1ilem  30854  ipasslem10  30867  normlem6  31143  dfhnorm2  31150  h1de2i  31581  spansnji  31674  pjneli  31751  mayetes3i  31757  pjclem1  32223  mdslmd3i  32360  atabsi  32429  imadifxp  32620  dfdec100  32836  dpmul100  32863  dpmul1000  32865  dpmul4  32880  xrge00  32999  cyc2fv1  33123  cyc2fv2  33124  cyc3fv3  33141  opprlidlabs  33492  locfinref  33801  cnvordtrestixx  33873  raddcn  33889  rrhcn  33959  qqtopn  33973  esumpfinvallem  34054  sxbrsigalem1  34266  eulerpartgbij  34353  sgnneg  34521  hgt750lem2  34645  subfacp1lem1  35163  subfacval2  35171  quad3  35654  ptrest  37605  poimirlem3  37609  poimirlem8  37614  poimirlem15  37621  mblfinlem3  37645  ismblfin  37647  areacirc  37699  pmapglb  39752  dvh4dimN  41429  hdmapfval  41809  12gcd5e1  41984  sqdeccom12  42302  readvrec  42370  remul02  42411  mapfzcons1  42704  lmhmlnmsplit  43075  pwssplit4  43077  clcnvlem  43612  cnvrcl0  43614  sqrtcval2  43631  resqrtvalex  43634  imsqrtvalex  43635  iunrelexp0  43691  sumnnodd  45585  climinf2mpt  45669  climinfmpt  45670  dvnmul  45898  wallispilem4  46023  dirkertrigeqlem3  46055  fourierdlem24  46086  fourierdlem57  46118  fourierdlem58  46119  fourierdlem80  46141  fourierswlem  46185  fouriersw  46186  fouriercn  46187  subsaliuncl  46313  gsumge0cl  46326  sge0tsms  46335  caragenuncllem  46467  0ome  46484  hoidmvle  46555  ovolval3  46602  ovolval4lem1  46604  smfpimbor1lem2  46754  gbpart7  47691  gbpart9  47693  gbpart11  47694  nnsum3primes4  47712  xpiun  48001  lindslinindsimp2lem5  48307  ackval42a  48546  aacllem  49031