Theorem eqtr2i 2226

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtrri  2230  3eqtr2ri  2232  symdif1  3437  dfif3  3583  dfsn2  3646  prprc1  3740  ruv  4597  xpindi  4812  xpindir  4813  dmcnvcnv  4901  rncnvcnv  4902  imainrect  5127  dfrn4  5142  fcoi1  5455  foimacnv  5539  fsnunfv  5784  dfoprab3  6276  fiintim  7027  sbthlemi8  7065  pitonnlem1  7957  ixi  8655  recexaplem2  8724  zeo  9477  num0h  9514  dec10p  9545  fseq1p1m1  10215  fsumrelem  11724  ef0lem  11913  ef01bndlem  12009  3lcm2e6woprm  12350  strsl0  12823  0g0  13150  tgioo  14968  tgqioo  14969  dveflem  15140  sincos4thpi  15254  coskpi  15262