Theorem eqtr2i 2793

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  3eqtrri  2797  3eqtr2ri  2799  dfun3  4237  dfif3  4504  dfsn2  4604  prprc1  4733  diftpsn3  4771  ssunpr  4800  sstp  4802  unidif0OLD  5329  xpindi  5817  xpindir  5818  dmcnvcnv  5921  rncnvcnv  5922  imainrect  6178  dfrn4  6200  predres  6337  fcoi1  6750  foimacnv  6836  f1ossf1o  7122  fsnunfv  7183  difex2  7755  dfoprab3  8047  offval22  8079  suppvalbr  8156  fvmpocurryd  8263  mapsnconst  8886  sbthlem8  9078  fiint  9282  ordtypecbv  9475  trcl  9693  rankxplim2  9848  infdju1  10169  cfval2  10240  itunitc  10401  ituniiun  10402  hsmex2  10413  ltexnq  10956  ixi  11839  zeo  12678  num0h  12719  dec10p  12755  fseq1p1m1  13622  cats1fvn  14891  s3fn  14944  sgnneg  15133  fsumrelem  15855  ef0lem  16128  ef01bndlem  16236  sadcadd  16512  sadadd2  16514  3lcm2e6woprm  16669  mod2xnegi  17127  str0  17245  ressinbas  17301  mreexexlem4d  17699  0g0  18718  frmdplusg  18909  smndex1bas  18964  sgrp2nmndlem4  18986  sgrp2nmndlem5  18987  oppgplusfval  19414  symgsubmefmnd  19464  psgnsn  19586  psgnprfval1  19588  frgpnabllem1  19939  opprmulfval  20417  opprrngb  20424  opprringb  20426  opprunit  20455  00lsp  21076  chrval  21638  dsmmelbas  21854  ltbwe  22160  ply1plusgfvi  22366  mat2pmatfval  22845  unisngl  23649  qtopres  23820  ufildr  24053  oppgtmd  24219  tgioo  24918  tgqioo  24922  dveflem  26103  lhop1lem  26137  sincos4thpi  26640  coskpi  26650  cxpsqrtlem  26829  log2ublem1  27073  efrlim  27096  basellem3  27209  bposlem9  27418  madeun  28039  precsexlem11  28372  graop  29316  0grsubgr  29565  usgrfilem  29614  finsumvtxdg2ssteplem4  29835  wlkvtxedg  29930  2wlkdlem1  30211  2pthd  30226  wlk2v2e  30445  3wlkdlem1  30447  3pthd  30462  konigsberg  30545  cnidOLD  30871  ip1ilem  31115  ipasslem10  31128  normlem6  31404  dfhnorm2  31411  h1de2i  31842  spansnji  31935  pjneli  32012  mayetes3i  32018  pjclem1  32484  mdslmd3i  32621  atabsi  32690  imadifxp  32883  dfdec100  33111  dpmul100  33153  dpmul1000  33155  dpmul4  33170  xrge00  33271  cyc2fv1  33378  cyc2fv2  33379  cyc3fv3  33396  opprlidlabs  33708  vieta  33911  cos9thpiminplylem5  34117  locfinref  34172  cnvordtrestixx  34244  raddcn  34260  rrhcn  34328  qqtopn  34342  esumpfinvallem  34405  sxbrsigalem1  34616  eulerpartgbij  34703  hgt750lem2  34980  subfacp1lem1  35566  subfacval2  35574  quad3  36057  ptrest  38153  poimirlem3  38157  poimirlem8  38162  poimirlem15  38169  mblfinlem3  38193  ismblfin  38195  areacirc  38247  pmapglb  40429  dvh4dimN  42106  hdmapfval  42486  12gcd5e1  42655  sqdeccom12  42933  remul02  43049  mapfzcons1  43333  lmhmlnmsplit  43699  pwssplit4  43701  clcnvlem  44234  cnvrcl0  44236  sqrtcval2  44253  resqrtvalex  44256  imsqrtvalex  44257  iunrelexp0  44313  sumnnodd  46231  climinf2mpt  46313  climinfmpt  46314  dvnmul  46542  wallispilem4  46667  dirkertrigeqlem3  46699  fourierdlem24  46730  fourierdlem57  46762  fourierdlem58  46763  fourierdlem80  46785  fourierswlem  46829  fouriersw  46830  fouriercn  46831  subsaliuncl  46957  gsumge0cl  46970  sge0tsms  46979  caragenuncllem  47111  0ome  47128  hoidmvle  47199  ovolval3  47246  ovolval4lem1  47248  smfpimbor1lem2  47398  gbpart7  48414  gbpart9  48416  gbpart11  48417  nnsum3primes4  48435  gpg5edgnedg  48777  xpiun  48805  lindslinindsimp2lem5  49120  ackval42a  49355  aacllem  50457