Theorem eqtr2i 2759

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  3eqtrri  2763  3eqtr2ri  2765  dfun3  4266  dfif3  4543  dfsn2  4642  prprc1  4770  diftpsn3  4806  ssunpr  4836  sstp  4838  unidif0  5359  xpindi  5834  xpindir  5835  dmcnvcnv  5933  rncnvcnv  5934  imainrect  6181  dfrn4  6202  predres  6341  fcoi1  6766  foimacnv  6851  f1ossf1o  7129  fsnunfv  7188  difex2  7751  dfoprab3  8044  offval22  8078  suppvalbr  8154  fvmpocurryd  8260  mapsnconst  8890  sbthlem8  9094  fiint  9328  ordtypecbv  9516  trcl  9727  rankxplim2  9879  infdju1  10188  cfval2  10259  itunitc  10420  ituniiun  10421  hsmex2  10432  ltexnq  10974  ixi  11849  zeo  12654  num0h  12695  dec10p  12726  fseq1p1m1  13581  cats1fvn  14815  s3fn  14868  fsumrelem  15759  ef0lem  16028  ef01bndlem  16133  sadcadd  16405  sadadd2  16407  3lcm2e6woprm  16558  mod2xnegi  17010  decexp2  17014  str0  17128  ressinbas  17196  mreexexlem4d  17597  0g0  18591  frmdplusg  18773  smndex1bas  18825  sgrp2nmndlem4  18847  sgrp2nmndlem5  18848  oppgplusfval  19255  symgsubmefmnd  19309  psgnsn  19431  psgnprfval1  19433  frgpnabllem1  19784  opprmulfval  20229  opprrngb  20239  opprringb  20241  opprunit  20270  00lsp  20738  chrval  21298  dsmmelbas  21515  ltbwe  21820  ply1plusgfvi  21986  mat2pmatfval  22447  unisngl  23253  qtopres  23424  ufildr  23657  oppgtmd  23823  tgioo  24534  tgqioo  24538  dveflem  25730  lhop1lem  25764  sincos4thpi  26257  coskpi  26266  cxpsqrtlem  26444  log2ublem1  26685  efrlim  26708  basellem3  26821  bposlem9  27029  madeun  27613  precsexlem11  27900  graop  28554  0grsubgr  28800  usgrfilem  28849  finsumvtxdg2ssteplem4  29070  wlkvtxedg  29166  2wlkdlem1  29444  2pthd  29459  wlk2v2e  29675  3wlkdlem1  29677  3pthd  29692  konigsberg  29775  cnidOLD  30100  ip1ilem  30344  ipasslem10  30357  normlem6  30633  dfhnorm2  30640  h1de2i  31071  spansnji  31164  pjneli  31241  mayetes3i  31247  pjclem1  31713  mdslmd3i  31850  atabsi  31919  imadifxp  32097  dfdec100  32301  dpmul100  32328  dpmul1000  32330  dpmul4  32345  xrge00  32452  cyc2fv1  32548  cyc2fv2  32549  cyc3fv3  32566  opprlidlabs  32871  locfinref  33117  cnvordtrestixx  33189  raddcn  33205  rrhcn  33273  qqtopn  33287  esumpfinvallem  33368  sxbrsigalem1  33580  eulerpartgbij  33667  sgnneg  33835  hgt750lem2  33960  subfacp1lem1  34466  subfacval2  34474  quad3  34951  ptrest  36792  poimirlem3  36796  poimirlem8  36801  poimirlem15  36808  mblfinlem3  36832  ismblfin  36834  areacirc  36886  pmapglb  38946  dvh4dimN  40623  hdmapfval  41003  12gcd5e1  41176  sqdeccom12  41505  remul02  41582  mapfzcons1  41759  lmhmlnmsplit  42133  pwssplit4  42135  clcnvlem  42678  cnvrcl0  42680  sqrtcval2  42697  resqrtvalex  42700  imsqrtvalex  42701  iunrelexp0  42757  sumnnodd  44646  climinf2mpt  44730  climinfmpt  44731  dvnmul  44959  wallispilem4  45084  dirkertrigeqlem3  45116  fourierdlem24  45147  fourierdlem57  45179  fourierdlem58  45180  fourierdlem80  45202  fourierswlem  45246  fouriersw  45247  fouriercn  45248  subsaliuncl  45374  gsumge0cl  45387  sge0tsms  45396  caragenuncllem  45528  0ome  45545  hoidmvle  45616  ovolval3  45663  ovolval4lem1  45665  smfpimbor1lem2  45815  gbpart7  46735  gbpart9  46737  gbpart11  46738  nnsum3primes4  46756  xpiun  46836  lindslinindsimp2lem5  47232  ackval42a  47472  aacllem  47937