Theorem eqtr2i 2785

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 2784	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2770	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 2733

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

This theorem is used by:  3eqtrri  2789  3eqtr2ri  2791  dfun3  4222  dfif3  4497  dfsn2  4597  prprc1  4726  diftpsn3  4765  ssunpr  4794  sstp  4796  unidif0OLD  5322  xpindi  5810  xpindir  5811  dmcnvcnv  5915  rncnvcnv  5916  imainrect  6173  dfrn4  6197  imadifssranOLD  6203  predres  6343  fcoi1  6757  foimacnv  6843  f1ossf1o  7130  fsnunfv  7193  difex2  7775  dfoprab3  8066  offval22  8100  suppvalbr  8182  fvmpocurryd  8289  mapsnconst  8921  sbthlem8  9114  fiint  9319  ordtypecbv  9512  trcl  9730  rankxplim2  9898  infdju1  10269  cfval2  10339  itunitc  10500  ituniiun  10501  hsmex2  10512  ltexnq  11061  ixi  11946  zeo  12786  num0h  12827  dec10p  12863  fseq1p1m1  13733  cats1fvn  15010  s3fn  15063  sgnneg  15254  fsumrelem  15975  ef0lem  16245  ef01bndlem  16353  sadcadd  16629  sadadd2  16631  3lcm2e6woprm  16791  mod2xnegi  17250  str0  17368  ressinbas  17424  mreexexlem4d  17822  0g0  18845  frmdplusg  19051  smndex1bas  19106  sgrp2nmndlem4  19128  sgrp2nmndlem5  19129  oppgplusfval  19563  symgsubmefmnd  19613  psgnsn  19735  psgnprfval1  19737  frgpnabllem1  20088  opprmulfval  20570  opprrngb  20577  opprringb  20579  opprunit  20608  isdrng3lem1  21006  00lsp  21257  rspvalint  21524  chrval  21830  dsmmelbas  22046  ltbwe  22354  ply1plusgfvi  22560  mat2pmatfval  23042  unisngl  23847  qtopres  24018  ufildr  24251  oppgtmd  24417  tgioo  25116  tgqioo  25120  dveflem  26300  lhop1lem  26334  sincos4thpi  26843  coskpi  26852  cxpsqrtlem  27031  log2ublem1  27275  efrlim  27298  basellem3  27411  bposlem9  27620  madeun  28271  precsexlem11  28604  graop  29608  0grsubgr  29860  usgrfilem  29909  finsumvtxdg2ssteplem4  30130  wlkvtxedg  30225  2wlkdlem1  30515  2pthd  30530  wlk2v2e  30759  3wlkdlem1  30761  3pthd  30776  konigsberg  30859  cnidOLD  31185  ip1ilem  31429  ipasslem10  31442  normlem6  31718  dfhnorm2  31725  h1de2i  32156  spansnji  32249  pjneli  32326  mayetes3i  32332  pjclem1  32798  mdslmd3i  32935  atabsi  33004  imadifxp  33196  dfdec100  33422  dpmul100  33464  dpmul1000  33466  dpmul4  33481  xrge00  33576  cyc2fv1  33683  cyc2fv2  33684  cyc3fv3  33701  opprlidlabs  34010  vieta  34213  cos9thpiminplylem5  34419  locfinref  34474  cnvordtrestixx  34546  raddcn  34562  rrhcn  34630  qqtopn  34644  esumpfinvallem  34707  sxbrsigalem1  34918  eulerpartgbij  35005  hgt750lem2  35282  subfacp1lem1  35945  subfacval2  35953  quad3  36436  ptrest  38539  poimirlem3  38543  poimirlem8  38548  poimirlem15  38555  mblfinlem3  38579  ismblfin  38581  areacirc  38633  pmapglb  40829  dvh4dimN  42506  hdmapfval  42886  12gcd5e1  43055  sqdeccom12  43348  remul02  43458  mapfzcons1  43729  lmhmlnmsplit  44090  pwssplit4  44092  clcnvlem  44624  cnvrcl0  44626  sqrtcval2  44643  resqrtvalex  44646  imsqrtvalex  44647  iunrelexp0  44703  sumnnodd  46643  climinf2mpt  46725  climinfmpt  46726  dvnmul  46954  wallispilem4  47079  dirkertrigeqlem3  47111  fourierdlem24  47142  fourierdlem57  47174  fourierdlem58  47175  fourierdlem80  47197  fourierswlem  47241  fouriersw  47242  fouriercn  47243  subsaliuncl  47369  gsumge0cl  47382  sge0tsms  47391  caragenuncllem  47523  0ome  47540  hoidmvle  47611  ovolval3  47658  ovolval4lem1  47660  smfpimbor1lem2  47810  goldpolyfactor  47928  sqrtnpoly  47944  gbpart7  48866  gbpart9  48868  gbpart11  48869  nnsum3primes4  48887  gpg5edgnedg  49229  xpiun  49257  lindslinindsimp2lem5  49575  ackval42a  49810  aacllem  50940