Theorem eqtr2i 2789

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  3eqtrri  2793  3eqtr2ri  2795  dfun3  4229  dfif3  4504  dfsn2  4604  prprc1  4733  diftpsn3  4772  ssunpr  4801  sstp  4803  unidif0OLD  5333  xpindi  5821  xpindir  5822  dmcnvcnv  5925  rncnvcnv  5926  imainrect  6181  dfrn4  6203  imadifssran  6204  predres  6344  fcoi1  6756  foimacnv  6842  f1ossf1o  7128  fsnunfv  7189  difex2  7761  dfoprab3  8053  offval22  8085  suppvalbr  8162  fvmpocurryd  8269  mapsnconst  8892  sbthlem8  9085  fiint  9289  ordtypecbv  9482  trcl  9700  rankxplim2  9855  infdju1  10185  cfval2  10255  itunitc  10416  ituniiun  10417  hsmex2  10428  ltexnq  10971  ixi  11854  zeo  12694  num0h  12735  dec10p  12771  fseq1p1m1  13639  cats1fvn  14915  s3fn  14968  sgnneg  15157  fsumrelem  15878  ef0lem  16150  ef01bndlem  16258  sadcadd  16534  sadadd2  16536  3lcm2e6woprm  16691  mod2xnegi  17149  str0  17267  ressinbas  17323  mreexexlem4d  17721  0g0  18740  frmdplusg  18937  smndex1bas  18992  sgrp2nmndlem4  19014  sgrp2nmndlem5  19015  oppgplusfval  19442  symgsubmefmnd  19492  psgnsn  19614  psgnprfval1  19616  frgpnabllem1  19967  opprmulfval  20447  opprrngb  20454  opprringb  20456  opprunit  20485  isdrng3lem1  20881  00lsp  21132  rspvalint  21399  chrval  21703  dsmmelbas  21919  ltbwe  22225  ply1plusgfvi  22431  mat2pmatfval  22910  unisngl  23715  qtopres  23886  ufildr  24119  oppgtmd  24285  tgioo  24984  tgqioo  24988  dveflem  26169  lhop1lem  26203  sincos4thpi  26709  coskpi  26719  cxpsqrtlem  26898  log2ublem1  27142  efrlim  27165  basellem3  27278  bposlem9  27487  madeun  28108  precsexlem11  28441  graop  29410  0grsubgr  29662  usgrfilem  29711  finsumvtxdg2ssteplem4  29932  wlkvtxedg  30027  2wlkdlem1  30317  2pthd  30332  wlk2v2e  30555  3wlkdlem1  30557  3pthd  30572  konigsberg  30655  cnidOLD  30981  ip1ilem  31225  ipasslem10  31238  normlem6  31514  dfhnorm2  31521  h1de2i  31952  spansnji  32045  pjneli  32122  mayetes3i  32128  pjclem1  32594  mdslmd3i  32731  atabsi  32800  imadifxp  32993  dfdec100  33220  dpmul100  33262  dpmul1000  33264  dpmul4  33279  xrge00  33374  cyc2fv1  33481  cyc2fv2  33482  cyc3fv3  33499  opprlidlabs  33807  vieta  34010  cos9thpiminplylem5  34216  locfinref  34271  cnvordtrestixx  34343  raddcn  34359  rrhcn  34427  qqtopn  34441  esumpfinvallem  34504  sxbrsigalem1  34716  eulerpartgbij  34803  hgt750lem2  35080  subfacp1lem1  35684  subfacval2  35692  quad3  36175  ptrest  38303  poimirlem3  38307  poimirlem8  38312  poimirlem15  38319  mblfinlem3  38343  ismblfin  38345  areacirc  38397  pmapglb  40577  dvh4dimN  42254  hdmapfval  42634  12gcd5e1  42803  sqdeccom12  43083  remul02  43199  mapfzcons1  43481  lmhmlnmsplit  43847  pwssplit4  43849  clcnvlem  44382  cnvrcl0  44384  sqrtcval2  44401  resqrtvalex  44404  imsqrtvalex  44405  iunrelexp0  44461  sumnnodd  46379  climinf2mpt  46461  climinfmpt  46462  dvnmul  46690  wallispilem4  46815  dirkertrigeqlem3  46847  fourierdlem24  46878  fourierdlem57  46910  fourierdlem58  46911  fourierdlem80  46933  fourierswlem  46977  fouriersw  46978  fouriercn  46979  subsaliuncl  47105  gsumge0cl  47118  sge0tsms  47127  caragenuncllem  47259  0ome  47276  hoidmvle  47347  ovolval3  47394  ovolval4lem1  47396  smfpimbor1lem2  47546  gbpart7  48565  gbpart9  48567  gbpart11  48568  nnsum3primes4  48586  gpg5edgnedg  48928  xpiun  48956  lindslinindsimp2lem5  49275  ackval42a  49510  aacllem  50654