Theorem eqtr2i 2755

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  3eqtrri  2759  3eqtr2ri  2761  dfun3  4221  dfif3  4485  dfsn2  4584  prprc1  4713  diftpsn3  4749  ssunpr  4781  sstp  4783  unidif0  5293  xpindi  5768  xpindir  5769  dmcnvcnv  5868  rncnvcnv  5869  imainrect  6123  dfrn4  6144  predres  6281  fcoi1  6692  foimacnv  6775  f1ossf1o  7056  fsnunfv  7116  difex2  7688  dfoprab3  7981  offval22  8013  suppvalbr  8089  fvmpocurryd  8196  mapsnconst  8811  sbthlem8  9002  fiint  9206  ordtypecbv  9398  trcl  9613  rankxplim2  9768  infdju1  10076  cfval2  10146  itunitc  10307  ituniiun  10308  hsmex2  10319  ltexnq  10861  ixi  11741  zeo  12554  num0h  12595  dec10p  12626  fseq1p1m1  13493  cats1fvn  14760  s3fn  14813  fsumrelem  15709  ef0lem  15980  ef01bndlem  16088  sadcadd  16364  sadadd2  16366  3lcm2e6woprm  16521  mod2xnegi  16978  str0  17095  ressinbas  17151  mreexexlem4d  17548  0g0  18567  frmdplusg  18757  smndex1bas  18809  sgrp2nmndlem4  18831  sgrp2nmndlem5  18832  oppgplusfval  19255  symgsubmefmnd  19305  psgnsn  19427  psgnprfval1  19429  frgpnabllem1  19780  opprmulfval  20252  opprrngb  20259  opprringb  20261  opprunit  20290  00lsp  20909  chrval  21455  dsmmelbas  21671  ltbwe  21974  ply1plusgfvi  22149  mat2pmatfval  22633  unisngl  23437  qtopres  23608  ufildr  23841  oppgtmd  24007  tgioo  24706  tgqioo  24710  dveflem  25905  lhop1lem  25940  sincos4thpi  26444  coskpi  26454  cxpsqrtlem  26633  log2ublem1  26878  efrlim  26901  efrlimOLD  26902  basellem3  27015  bposlem9  27225  madeun  27824  precsexlem11  28150  0reno  28394  graop  29002  0grsubgr  29251  usgrfilem  29300  finsumvtxdg2ssteplem4  29522  wlkvtxedg  29617  2wlkdlem1  29898  2pthd  29913  wlk2v2e  30129  3wlkdlem1  30131  3pthd  30146  konigsberg  30229  cnidOLD  30554  ip1ilem  30798  ipasslem10  30811  normlem6  31087  dfhnorm2  31094  h1de2i  31525  spansnji  31618  pjneli  31695  mayetes3i  31701  pjclem1  32167  mdslmd3i  32304  atabsi  32373  imadifxp  32573  dfdec100  32805  sgnneg  32808  dpmul100  32869  dpmul1000  32871  dpmul4  32886  xrge00  32987  cyc2fv1  33082  cyc2fv2  33083  cyc3fv3  33100  opprlidlabs  33442  cos9thpiminplylem5  33791  locfinref  33846  cnvordtrestixx  33918  raddcn  33934  rrhcn  34002  qqtopn  34016  esumpfinvallem  34079  sxbrsigalem1  34290  eulerpartgbij  34377  hgt750lem2  34657  subfacp1lem1  35215  subfacval2  35223  quad3  35706  ptrest  37659  poimirlem3  37663  poimirlem8  37668  poimirlem15  37675  mblfinlem3  37699  ismblfin  37701  areacirc  37753  pmapglb  39809  dvh4dimN  41486  hdmapfval  41866  12gcd5e1  42036  sqdeccom12  42322  remul02  42438  mapfzcons1  42750  lmhmlnmsplit  43120  pwssplit4  43122  clcnvlem  43656  cnvrcl0  43658  sqrtcval2  43675  resqrtvalex  43678  imsqrtvalex  43679  iunrelexp0  43735  sumnnodd  45670  climinf2mpt  45752  climinfmpt  45753  dvnmul  45981  wallispilem4  46106  dirkertrigeqlem3  46138  fourierdlem24  46169  fourierdlem57  46201  fourierdlem58  46202  fourierdlem80  46224  fourierswlem  46268  fouriersw  46269  fouriercn  46270  subsaliuncl  46396  gsumge0cl  46409  sge0tsms  46418  caragenuncllem  46550  0ome  46567  hoidmvle  46638  ovolval3  46685  ovolval4lem1  46687  smfpimbor1lem2  46837  gbpart7  47798  gbpart9  47800  gbpart11  47801  nnsum3primes4  47819  gpg5edgnedg  48161  xpiun  48189  lindslinindsimp2lem5  48494  ackval42a  48729  aacllem  49833