Theorem eqtr2i 2769

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  3eqtrri  2773  3eqtr2ri  2775  dfun3  4205  dfif3  4479  dfsn2  4580  prprc1  4707  diftpsn3  4741  ssunpr  4771  sstp  4773  unidif0  5286  pwundifOLD  5487  xpindi  5741  xpindir  5742  dmcnvcnv  5841  rncnvcnv  5842  imainrect  6083  dfrn4  6104  predres  6241  fcoi1  6646  foimacnv  6731  f1ossf1o  6997  fsnunfv  7056  difex2  7604  dfoprab3  7887  offval22  7919  fvmpocurryd  8078  mapsnconst  8663  sbthlem8  8859  fiint  9069  ordtypecbv  9254  trcl  9486  rankxplim2  9639  infdju1  9946  cfval2  10017  itunitc  10178  ituniiun  10179  hsmex2  10190  ltexnq  10732  ixi  11604  zeo  12406  num0h  12448  dec10p  12479  fseq1p1m1  13329  cats1fvn  14569  s3fn  14622  fsumrelem  15517  ef0lem  15786  ef01bndlem  15891  sadcadd  16163  sadadd2  16165  3lcm2e6woprm  16318  mod2xnegi  16770  decexp2  16774  str0  16888  ressinbas  16953  mreexexlem4d  17354  0g0  18346  frmdplusg  18491  smndex1bas  18543  sgrp2nmndlem4  18565  sgrp2nmndlem5  18566  oppgplusfval  18950  symgsubmefmnd  19004  psgnsn  19126  psgnprfval1  19128  frgpnabllem1  19472  opprmulfval  19862  opprringb  19872  opprunit  19901  00lsp  20241  chrval  20727  dsmmelbas  20944  ltbwe  21243  ply1plusgfvi  21411  mat2pmatfval  21870  unisngl  22676  qtopres  22847  ufildr  23080  oppgtmd  23246  tgioo  23957  tgqioo  23961  dveflem  25141  lhop1lem  25175  sincos4thpi  25668  coskpi  25677  cxpsqrtlem  25855  log2ublem1  26094  efrlim  26117  basellem3  26230  bposlem9  26438  graop  27397  0grsubgr  27643  usgrfilem  27692  finsumvtxdg2ssteplem4  27913  wlkvtxedg  28008  2wlkdlem1  28286  2pthd  28301  wlk2v2e  28517  3wlkdlem1  28519  3pthd  28534  konigsberg  28617  cnidOLD  28940  ip1ilem  29184  ipasslem10  29197  normlem6  29473  dfhnorm2  29480  h1de2i  29911  spansnji  30004  pjneli  30081  mayetes3i  30087  pjclem1  30553  mdslmd3i  30690  atabsi  30759  imadifxp  30936  dfdec100  31140  dpmul100  31167  dpmul1000  31169  dpmul4  31184  xrge00  31291  cyc2fv1  31384  cyc2fv2  31385  cyc3fv3  31402  locfinref  31787  cnvordtrestixx  31859  raddcn  31875  rrhcn  31943  qqtopn  31957  esumpfinvallem  32038  sxbrsigalem1  32248  eulerpartgbij  32335  sgnneg  32503  hgt750lem2  32628  subfacp1lem1  33137  subfacval2  33145  quad3  33624  madeun  34062  ptrest  35772  poimirlem3  35776  poimirlem8  35781  poimirlem15  35788  mblfinlem3  35812  ismblfin  35814  areacirc  35866  pmapglb  37780  dvh4dimN  39457  hdmapfval  39837  12gcd5e1  40008  sqdeccom12  40314  remul02  40385  mapfzcons1  40536  lmhmlnmsplit  40909  pwssplit4  40911  clcnvlem  41201  cnvrcl0  41203  sqrtcval2  41220  resqrtvalex  41223  imsqrtvalex  41224  iunrelexp0  41280  sumnnodd  43142  climinf2mpt  43226  climinfmpt  43227  dvnmul  43455  wallispilem4  43580  dirkertrigeqlem3  43612  fourierdlem24  43643  fourierdlem57  43675  fourierdlem58  43676  fourierdlem80  43698  fourierswlem  43742  fouriersw  43743  fouriercn  43744  subsaliuncl  43868  gsumge0cl  43880  sge0tsms  43889  caragenuncllem  44021  0ome  44038  hoidmvle  44109  ovolval3  44156  ovolval4lem1  44158  smfpimbor1lem2  44301  gbpart7  45188  gbpart9  45190  gbpart11  45191  nnsum3primes4  45209  xpiun  45289  lindslinindsimp2lem5  45772  ackval42a  46012  aacllem  46474