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  4596  xpindi  4811  xpindir  4812  dmcnvcnv  4900  rncnvcnv  4901  imainrect  5125  dfrn4  5140  fcoi1  5450  foimacnv  5534  fsnunfv  5775  dfoprab3  6267  fiintim  7010  sbthlemi8  7048  pitonnlem1  7940  ixi  8638  recexaplem2  8707  zeo  9460  num0h  9497  dec10p  9528  fseq1p1m1  10198  fsumrelem  11701  ef0lem  11890  ef01bndlem  11986  3lcm2e6woprm  12327  strsl0  12800  0g0  13126  tgioo  14944  tgqioo  14945  dveflem  15116  sincos4thpi  15230  coskpi  15238