Theorem eqtr2i 2218

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtrri  2222  3eqtr2ri  2224  symdif1  3429  dfif3  3575  dfsn2  3637  prprc1  3731  ruv  4587  xpindi  4802  xpindir  4803  dmcnvcnv  4891  rncnvcnv  4892  imainrect  5116  dfrn4  5131  fcoi1  5441  foimacnv  5525  fsnunfv  5766  dfoprab3  6258  fiintim  7001  sbthlemi8  7039  pitonnlem1  7931  ixi  8629  recexaplem2  8698  zeo  9450  num0h  9487  dec10p  9518  fseq1p1m1  10188  fsumrelem  11655  ef0lem  11844  ef01bndlem  11940  3lcm2e6woprm  12281  strsl0  12754  0g0  13080  tgioo  14898  tgqioo  14899  dveflem  15070  sincos4thpi  15184  coskpi  15192