Theorem eqtr2i 2121

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

Syntax hints:   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  3eqtrri  2125  3eqtr2ri  2127  symdif1  3288  dfif3  3434  dfsn2  3488  prprc1  3578  ruv  4403  xpindi  4612  xpindir  4613  dmcnvcnv  4701  rncnvcnv  4702  imainrect  4920  dfrn4  4935  fcoi1  5239  foimacnv  5319  fsnunfv  5553  dfoprab3  6019  fiintim  6746  sbthlemi8  6780  pitonnlem1  7532  ixi  8211  recexaplem2  8274  zeo  9008  num0h  9045  dec10p  9076  fseq1p1m1  9715  fsumrelem  11079  ef0lem  11164  ef01bndlem  11261  3lcm2e6woprm  11560  strsl0  11789  tgioo  12465  tgqioo  12466