Theorem eqtr2i 2253

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

Syntax hints:   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  3eqtrri  2257  3eqtr2ri  2259  symdif1  3474  dfif3  3623  dfsn2  3687  prprc1  3784  ruv  4654  xpindi  4871  xpindir  4872  dmcnvcnv  4962  rncnvcnv  4963  imainrect  5189  dfrn4  5204  fcoi1  5525  foimacnv  5610  fsnunfv  5863  dfoprab3  6363  fiintim  7166  sbthlemi8  7206  pitonnlem1  8108  ixi  8805  recexaplem2  8874  zeo  9629  num0h  9666  dec10p  9697  fseq1p1m1  10374  cats1fvn  11394  fsumrelem  12095  ef0lem  12284  ef01bndlem  12380  3lcm2e6woprm  12721  strsl0  13194  0g0  13522  tgioo  15348  tgqioo  15349  dveflem  15520  sincos4thpi  15634  coskpi  15642  0grsubgr  16188  konigsberglem5  16416  konigsberg  16417