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 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  3eqtrri  2764  3eqtr2ri  2766  dfun3  4228  dfif3  4494  dfsn2  4593  prprc1  4722  diftpsn3  4758  ssunpr  4790  sstp  4792  unidif0  5305  xpindi  5782  xpindir  5783  dmcnvcnv  5882  rncnvcnv  5883  imainrect  6139  dfrn4  6160  predres  6297  fcoi1  6708  foimacnv  6791  f1ossf1o  7073  fsnunfv  7133  difex2  7705  dfoprab3  7998  offval22  8030  suppvalbr  8106  fvmpocurryd  8213  mapsnconst  8830  sbthlem8  9022  fiint  9227  ordtypecbv  9422  trcl  9637  rankxplim2  9792  infdju1  10100  cfval2  10170  itunitc  10331  ituniiun  10332  hsmex2  10343  ltexnq  10886  ixi  11766  zeo  12578  num0h  12619  dec10p  12650  fseq1p1m1  13514  cats1fvn  14781  s3fn  14834  fsumrelem  15730  ef0lem  16001  ef01bndlem  16109  sadcadd  16385  sadadd2  16387  3lcm2e6woprm  16542  mod2xnegi  16999  str0  17116  ressinbas  17172  mreexexlem4d  17570  0g0  18589  frmdplusg  18779  smndex1bas  18831  sgrp2nmndlem4  18853  sgrp2nmndlem5  18854  oppgplusfval  19277  symgsubmefmnd  19327  psgnsn  19449  psgnprfval1  19451  frgpnabllem1  19802  opprmulfval  20275  opprrngb  20282  opprringb  20284  opprunit  20313  00lsp  20932  chrval  21478  dsmmelbas  21694  ltbwe  21999  ply1plusgfvi  22182  mat2pmatfval  22667  unisngl  23471  qtopres  23642  ufildr  23875  oppgtmd  24041  tgioo  24740  tgqioo  24744  dveflem  25939  lhop1lem  25974  sincos4thpi  26478  coskpi  26488  cxpsqrtlem  26667  log2ublem1  26912  efrlim  26935  efrlimOLD  26936  basellem3  27049  bposlem9  27259  madeun  27880  precsexlem11  28213  graop  29102  0grsubgr  29351  usgrfilem  29400  finsumvtxdg2ssteplem4  29622  wlkvtxedg  29717  2wlkdlem1  29998  2pthd  30013  wlk2v2e  30232  3wlkdlem1  30234  3pthd  30249  konigsberg  30332  cnidOLD  30657  ip1ilem  30901  ipasslem10  30914  normlem6  31190  dfhnorm2  31197  h1de2i  31628  spansnji  31721  pjneli  31798  mayetes3i  31804  pjclem1  32270  mdslmd3i  32407  atabsi  32476  imadifxp  32676  dfdec100  32911  sgnneg  32914  dpmul100  32978  dpmul1000  32980  dpmul4  32995  xrge00  33096  cyc2fv1  33203  cyc2fv2  33204  cyc3fv3  33221  opprlidlabs  33566  vieta  33736  cos9thpiminplylem5  33943  locfinref  33998  cnvordtrestixx  34070  raddcn  34086  rrhcn  34154  qqtopn  34168  esumpfinvallem  34231  sxbrsigalem1  34442  eulerpartgbij  34529  hgt750lem2  34809  subfacp1lem1  35373  subfacval2  35381  quad3  35864  ptrest  37820  poimirlem3  37824  poimirlem8  37829  poimirlem15  37836  mblfinlem3  37860  ismblfin  37862  areacirc  37914  pmapglb  40030  dvh4dimN  41707  hdmapfval  42087  12gcd5e1  42257  sqdeccom12  42544  remul02  42660  mapfzcons1  42959  lmhmlnmsplit  43329  pwssplit4  43331  clcnvlem  43864  cnvrcl0  43866  sqrtcval2  43883  resqrtvalex  43886  imsqrtvalex  43887  iunrelexp0  43943  sumnnodd  45876  climinf2mpt  45958  climinfmpt  45959  dvnmul  46187  wallispilem4  46312  dirkertrigeqlem3  46344  fourierdlem24  46375  fourierdlem57  46407  fourierdlem58  46408  fourierdlem80  46430  fourierswlem  46474  fouriersw  46475  fouriercn  46476  subsaliuncl  46602  gsumge0cl  46615  sge0tsms  46624  caragenuncllem  46756  0ome  46773  hoidmvle  46844  ovolval3  46891  ovolval4lem1  46893  smfpimbor1lem2  47043  gbpart7  48013  gbpart9  48015  gbpart11  48016  nnsum3primes4  48034  gpg5edgnedg  48376  xpiun  48404  lindslinindsimp2lem5  48708  ackval42a  48943  aacllem  50046