Theorem eqtr2i 2753

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 2752	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2738	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eqtrri  2757  3eqtr2ri  2759  dfun3  4229  dfif3  4493  dfsn2  4592  prprc1  4719  diftpsn3  4756  ssunpr  4788  sstp  4790  unidif0  5302  xpindi  5780  xpindir  5781  dmcnvcnv  5879  rncnvcnv  5880  imainrect  6134  dfrn4  6155  predres  6291  fcoi1  6702  foimacnv  6785  f1ossf1o  7066  fsnunfv  7127  difex2  7700  dfoprab3  7996  offval22  8028  suppvalbr  8104  fvmpocurryd  8211  mapsnconst  8826  sbthlem8  9018  fiint  9235  fiintOLD  9236  ordtypecbv  9428  trcl  9643  rankxplim2  9795  infdju1  10103  cfval2  10173  itunitc  10334  ituniiun  10335  hsmex2  10346  ltexnq  10888  ixi  11768  zeo  12581  num0h  12622  dec10p  12653  fseq1p1m1  13520  cats1fvn  14784  s3fn  14837  fsumrelem  15733  ef0lem  16004  ef01bndlem  16112  sadcadd  16388  sadadd2  16390  3lcm2e6woprm  16545  mod2xnegi  17002  str0  17119  ressinbas  17175  mreexexlem4d  17572  0g0  18557  frmdplusg  18747  smndex1bas  18799  sgrp2nmndlem4  18821  sgrp2nmndlem5  18822  oppgplusfval  19246  symgsubmefmnd  19296  psgnsn  19418  psgnprfval1  19420  frgpnabllem1  19771  opprmulfval  20243  opprrngb  20250  opprringb  20252  opprunit  20281  00lsp  20903  chrval  21449  dsmmelbas  21665  ltbwe  21968  ply1plusgfvi  22143  mat2pmatfval  22627  unisngl  23431  qtopres  23602  ufildr  23835  oppgtmd  24001  tgioo  24701  tgqioo  24705  dveflem  25900  lhop1lem  25935  sincos4thpi  26439  coskpi  26449  cxpsqrtlem  26628  log2ublem1  26873  efrlim  26896  efrlimOLD  26897  basellem3  27010  bposlem9  27220  madeun  27817  precsexlem11  28143  0reno  28385  graop  28993  0grsubgr  29242  usgrfilem  29291  finsumvtxdg2ssteplem4  29513  wlkvtxedg  29608  2wlkdlem1  29889  2pthd  29904  wlk2v2e  30120  3wlkdlem1  30122  3pthd  30137  konigsberg  30220  cnidOLD  30545  ip1ilem  30789  ipasslem10  30802  normlem6  31078  dfhnorm2  31085  h1de2i  31516  spansnji  31609  pjneli  31686  mayetes3i  31692  pjclem1  32158  mdslmd3i  32295  atabsi  32364  imadifxp  32564  dfdec100  32794  sgnneg  32797  dpmul100  32856  dpmul1000  32858  dpmul4  32873  xrge00  32987  cyc2fv1  33082  cyc2fv2  33083  cyc3fv3  33100  opprlidlabs  33441  cos9thpiminplylem5  33772  locfinref  33827  cnvordtrestixx  33899  raddcn  33915  rrhcn  33983  qqtopn  33997  esumpfinvallem  34060  sxbrsigalem1  34272  eulerpartgbij  34359  hgt750lem2  34639  subfacp1lem1  35171  subfacval2  35179  quad3  35662  ptrest  37618  poimirlem3  37622  poimirlem8  37627  poimirlem15  37634  mblfinlem3  37658  ismblfin  37660  areacirc  37712  pmapglb  39769  dvh4dimN  41446  hdmapfval  41826  12gcd5e1  41996  sqdeccom12  42282  remul02  42398  mapfzcons1  42710  lmhmlnmsplit  43080  pwssplit4  43082  clcnvlem  43616  cnvrcl0  43618  sqrtcval2  43635  resqrtvalex  43638  imsqrtvalex  43639  iunrelexp0  43695  sumnnodd  45631  climinf2mpt  45715  climinfmpt  45716  dvnmul  45944  wallispilem4  46069  dirkertrigeqlem3  46101  fourierdlem24  46132  fourierdlem57  46164  fourierdlem58  46165  fourierdlem80  46187  fourierswlem  46231  fouriersw  46232  fouriercn  46233  subsaliuncl  46359  gsumge0cl  46372  sge0tsms  46381  caragenuncllem  46513  0ome  46530  hoidmvle  46601  ovolval3  46648  ovolval4lem1  46650  smfpimbor1lem2  46800  gbpart7  47771  gbpart9  47773  gbpart11  47774  nnsum3primes4  47792  gpg5edgnedg  48134  xpiun  48162  lindslinindsimp2lem5  48467  ackval42a  48702  aacllem  49806