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  6195  imadifssranOLD  6201  predres  6341  fcoi1  6754  foimacnv  6840  f1ossf1o  7127  fsnunfv  7190  difex2  7772  dfoprab3  8063  offval22  8097  suppvalbr  8174  fvmpocurryd  8281  mapsnconst  8913  sbthlem8  9106  fiint  9311  ordtypecbv  9504  trcl  9722  rankxplim2  9890  infdju1  10261  cfval2  10331  itunitc  10492  ituniiun  10493  hsmex2  10504  ltexnq  11053  ixi  11938  zeo  12778  num0h  12819  dec10p  12855  fseq1p1m1  13725  cats1fvn  15002  s3fn  15055  sgnneg  15246  fsumrelem  15967  ef0lem  16237  ef01bndlem  16345  sadcadd  16621  sadadd2  16623  3lcm2e6woprm  16783  mod2xnegi  17242  str0  17360  ressinbas  17416  mreexexlem4d  17814  0g0  18837  frmdplusg  19043  smndex1bas  19098  sgrp2nmndlem4  19120  sgrp2nmndlem5  19121  oppgplusfval  19555  symgsubmefmnd  19605  psgnsn  19727  psgnprfval1  19729  frgpnabllem1  20080  opprmulfval  20562  opprrngb  20569  opprringb  20571  opprunit  20600  isdrng3lem1  20998  00lsp  21249  rspvalint  21516  chrval  21822  dsmmelbas  22038  ltbwe  22346  ply1plusgfvi  22552  mat2pmatfval  23034  unisngl  23839  qtopres  24010  ufildr  24243  oppgtmd  24409  tgioo  25108  tgqioo  25112  dveflem  26292  lhop1lem  26326  sincos4thpi  26835  coskpi  26844  cxpsqrtlem  27023  log2ublem1  27267  efrlim  27290  basellem3  27403  bposlem9  27612  madeun  28263  precsexlem11  28596  graop  29600  0grsubgr  29852  usgrfilem  29901  finsumvtxdg2ssteplem4  30122  wlkvtxedg  30217  2wlkdlem1  30507  2pthd  30522  wlk2v2e  30751  3wlkdlem1  30753  3pthd  30768  konigsberg  30851  cnidOLD  31177  ip1ilem  31421  ipasslem10  31434  normlem6  31710  dfhnorm2  31717  h1de2i  32148  spansnji  32241  pjneli  32318  mayetes3i  32324  pjclem1  32790  mdslmd3i  32927  atabsi  32996  imadifxp  33188  dfdec100  33414  dpmul100  33456  dpmul1000  33458  dpmul4  33473  xrge00  33568  cyc2fv1  33675  cyc2fv2  33676  cyc3fv3  33693  opprlidlabs  34002  vieta  34205  cos9thpiminplylem5  34411  locfinref  34466  cnvordtrestixx  34538  raddcn  34554  rrhcn  34622  qqtopn  34636  esumpfinvallem  34699  sxbrsigalem1  34910  eulerpartgbij  34997  hgt750lem2  35274  subfacp1lem1  35923  subfacval2  35931  quad3  36414  ptrest  38517  poimirlem3  38521  poimirlem8  38526  poimirlem15  38533  mblfinlem3  38557  ismblfin  38559  areacirc  38611  pmapglb  40807  dvh4dimN  42484  hdmapfval  42864  12gcd5e1  43033  sqdeccom12  43326  remul02  43436  mapfzcons1  43707  lmhmlnmsplit  44073  pwssplit4  44075  clcnvlem  44608  cnvrcl0  44610  sqrtcval2  44627  resqrtvalex  44630  imsqrtvalex  44631  iunrelexp0  44687  sumnnodd  46611  climinf2mpt  46693  climinfmpt  46694  dvnmul  46922  wallispilem4  47047  dirkertrigeqlem3  47079  fourierdlem24  47110  fourierdlem57  47142  fourierdlem58  47143  fourierdlem80  47165  fourierswlem  47209  fouriersw  47210  fouriercn  47211  subsaliuncl  47337  gsumge0cl  47350  sge0tsms  47359  caragenuncllem  47491  0ome  47508  hoidmvle  47579  ovolval3  47626  ovolval4lem1  47628  smfpimbor1lem2  47778  goldpolyfactor  47896  sqrtnpoly  47912  gbpart7  48834  gbpart9  48836  gbpart11  48837  nnsum3primes4  48855  gpg5edgnedg  49197  xpiun  49225  lindslinindsimp2lem5  49543  ackval42a  49778  aacllem  50908