Theorem eqtr2i 2759

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  3eqtrri  2763  3eqtr2ri  2765  dfun3  4251  dfif3  4515  dfsn2  4614  prprc1  4741  diftpsn3  4778  ssunpr  4810  sstp  4812  unidif0  5330  xpindi  5813  xpindir  5814  dmcnvcnv  5913  rncnvcnv  5914  imainrect  6170  dfrn4  6191  predres  6328  fcoi1  6751  foimacnv  6834  f1ossf1o  7117  fsnunfv  7178  difex2  7752  dfoprab3  8051  offval22  8085  suppvalbr  8161  fvmpocurryd  8268  mapsnconst  8904  sbthlem8  9102  fiint  9336  fiintOLD  9337  ordtypecbv  9529  trcl  9740  rankxplim2  9892  infdju1  10202  cfval2  10272  itunitc  10433  ituniiun  10434  hsmex2  10445  ltexnq  10987  ixi  11864  zeo  12677  num0h  12718  dec10p  12749  fseq1p1m1  13613  cats1fvn  14875  s3fn  14928  fsumrelem  15821  ef0lem  16092  ef01bndlem  16200  sadcadd  16475  sadadd2  16477  3lcm2e6woprm  16632  mod2xnegi  17089  str0  17206  ressinbas  17264  mreexexlem4d  17657  0g0  18640  frmdplusg  18830  smndex1bas  18882  sgrp2nmndlem4  18904  sgrp2nmndlem5  18905  oppgplusfval  19329  symgsubmefmnd  19377  psgnsn  19499  psgnprfval1  19501  frgpnabllem1  19852  opprmulfval  20297  opprrngb  20304  opprringb  20306  opprunit  20335  00lsp  20936  chrval  21482  dsmmelbas  21697  ltbwe  22000  ply1plusgfvi  22175  mat2pmatfval  22659  unisngl  23463  qtopres  23634  ufildr  23867  oppgtmd  24033  tgioo  24733  tgqioo  24737  dveflem  25933  lhop1lem  25968  sincos4thpi  26472  coskpi  26482  cxpsqrtlem  26661  log2ublem1  26906  efrlim  26929  efrlimOLD  26930  basellem3  27043  bposlem9  27253  madeun  27839  precsexlem11  28158  0reno  28346  graop  28954  0grsubgr  29203  usgrfilem  29252  finsumvtxdg2ssteplem4  29474  wlkvtxedg  29570  2wlkdlem1  29853  2pthd  29868  wlk2v2e  30084  3wlkdlem1  30086  3pthd  30101  konigsberg  30184  cnidOLD  30509  ip1ilem  30753  ipasslem10  30766  normlem6  31042  dfhnorm2  31049  h1de2i  31480  spansnji  31573  pjneli  31650  mayetes3i  31656  pjclem1  32122  mdslmd3i  32259  atabsi  32328  imadifxp  32528  dfdec100  32755  sgnneg  32758  dpmul100  32817  dpmul1000  32819  dpmul4  32834  xrge00  32953  cyc2fv1  33078  cyc2fv2  33079  cyc3fv3  33096  opprlidlabs  33446  cos9thpiminplylem5  33766  locfinref  33818  cnvordtrestixx  33890  raddcn  33906  rrhcn  33974  qqtopn  33988  esumpfinvallem  34051  sxbrsigalem1  34263  eulerpartgbij  34350  hgt750lem2  34630  subfacp1lem1  35147  subfacval2  35155  quad3  35638  ptrest  37589  poimirlem3  37593  poimirlem8  37598  poimirlem15  37605  mblfinlem3  37629  ismblfin  37631  areacirc  37683  pmapglb  39735  dvh4dimN  41412  hdmapfval  41792  12gcd5e1  41962  sqdeccom12  42286  remul02  42395  mapfzcons1  42687  lmhmlnmsplit  43058  pwssplit4  43060  clcnvlem  43594  cnvrcl0  43596  sqrtcval2  43613  resqrtvalex  43616  imsqrtvalex  43617  iunrelexp0  43673  sumnnodd  45607  climinf2mpt  45691  climinfmpt  45692  dvnmul  45920  wallispilem4  46045  dirkertrigeqlem3  46077  fourierdlem24  46108  fourierdlem57  46140  fourierdlem58  46141  fourierdlem80  46163  fourierswlem  46207  fouriersw  46208  fouriercn  46209  subsaliuncl  46335  gsumge0cl  46348  sge0tsms  46357  caragenuncllem  46489  0ome  46506  hoidmvle  46577  ovolval3  46624  ovolval4lem1  46626  smfpimbor1lem2  46776  gbpart7  47729  gbpart9  47731  gbpart11  47732  nnsum3primes4  47750  xpiun  48081  lindslinindsimp2lem5  48386  ackval42a  48625  aacllem  49613