Theorem eqtr2i 2784

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 2783	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2769	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 2155  ax-ext 2732

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

This theorem is used by:  3eqtrri  2788  3eqtr2ri  2790  dfun3  4222  dfif3  4497  dfsn2  4597  prprc1  4726  diftpsn3  4765  ssunpr  4794  sstp  4796  unidif0OLD  5325  xpindi  5813  xpindir  5814  dmcnvcnv  5917  rncnvcnv  5918  imainrect  6174  dfrn4  6196  imadifssran  6197  predres  6337  fcoi1  6749  foimacnv  6835  f1ossf1o  7122  fsnunfv  7185  difex2  7759  dfoprab3  8051  offval22  8085  suppvalbr  8162  fvmpocurryd  8269  mapsnconst  8899  sbthlem8  9092  fiint  9296  ordtypecbv  9489  trcl  9707  rankxplim2  9862  infdju1  10192  cfval2  10262  itunitc  10423  ituniiun  10424  hsmex2  10435  ltexnq  10984  ixi  11867  zeo  12707  num0h  12748  dec10p  12784  fseq1p1m1  13653  cats1fvn  14929  s3fn  14982  sgnneg  15173  fsumrelem  15894  ef0lem  16164  ef01bndlem  16272  sadcadd  16548  sadadd2  16550  3lcm2e6woprm  16705  mod2xnegi  17163  str0  17281  ressinbas  17337  mreexexlem4d  17735  0g0  18757  frmdplusg  18963  smndex1bas  19018  sgrp2nmndlem4  19040  sgrp2nmndlem5  19041  oppgplusfval  19475  symgsubmefmnd  19525  psgnsn  19647  psgnprfval1  19649  frgpnabllem1  20000  opprmulfval  20480  opprrngb  20487  opprringb  20489  opprunit  20518  isdrng3lem1  20914  00lsp  21165  rspvalint  21432  chrval  21736  dsmmelbas  21952  ltbwe  22260  ply1plusgfvi  22466  mat2pmatfval  22948  unisngl  23753  qtopres  23924  ufildr  24157  oppgtmd  24323  tgioo  25022  tgqioo  25026  dveflem  26206  lhop1lem  26240  sincos4thpi  26751  coskpi  26760  cxpsqrtlem  26939  log2ublem1  27183  efrlim  27206  basellem3  27319  bposlem9  27528  madeun  28149  precsexlem11  28482  graop  29486  0grsubgr  29738  usgrfilem  29787  finsumvtxdg2ssteplem4  30008  wlkvtxedg  30103  2wlkdlem1  30393  2pthd  30408  wlk2v2e  30637  3wlkdlem1  30639  3pthd  30654  konigsberg  30737  cnidOLD  31063  ip1ilem  31307  ipasslem10  31320  normlem6  31596  dfhnorm2  31603  h1de2i  32034  spansnji  32127  pjneli  32204  mayetes3i  32210  pjclem1  32676  mdslmd3i  32813  atabsi  32882  imadifxp  33074  dfdec100  33300  dpmul100  33342  dpmul1000  33344  dpmul4  33359  xrge00  33454  cyc2fv1  33561  cyc2fv2  33562  cyc3fv3  33579  opprlidlabs  33887  vieta  34090  cos9thpiminplylem5  34296  locfinref  34351  cnvordtrestixx  34423  raddcn  34439  rrhcn  34507  qqtopn  34521  esumpfinvallem  34584  sxbrsigalem1  34796  eulerpartgbij  34883  hgt750lem2  35160  subfacp1lem1  35758  subfacval2  35766  quad3  36249  ptrest  38368  poimirlem3  38372  poimirlem8  38377  poimirlem15  38384  mblfinlem3  38408  ismblfin  38410  areacirc  38462  pmapglb  40643  dvh4dimN  42320  hdmapfval  42700  12gcd5e1  42869  sqdeccom12  43164  remul02  43280  mapfzcons1  43562  lmhmlnmsplit  43928  pwssplit4  43930  clcnvlem  44463  cnvrcl0  44465  sqrtcval2  44482  resqrtvalex  44485  imsqrtvalex  44486  iunrelexp0  44542  sumnnodd  46460  climinf2mpt  46542  climinfmpt  46543  dvnmul  46771  wallispilem4  46896  dirkertrigeqlem3  46928  fourierdlem24  46959  fourierdlem57  46991  fourierdlem58  46992  fourierdlem80  47014  fourierswlem  47058  fouriersw  47059  fouriercn  47060  subsaliuncl  47186  gsumge0cl  47199  sge0tsms  47208  caragenuncllem  47340  0ome  47357  hoidmvle  47428  ovolval3  47475  ovolval4lem1  47477  smfpimbor1lem2  47627  goldpolyfactor  47745  sqrtnpoly  47761  gbpart7  48683  gbpart9  48685  gbpart11  48686  nnsum3primes4  48704  gpg5edgnedg  49046  xpiun  49074  lindslinindsimp2lem5  49392  ackval42a  49627  aacllem  50772