Theorem eqtr2i 2215

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 2214	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2197	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtrri  2219  3eqtr2ri  2221  symdif1  3425  dfif3  3571  dfsn2  3633  prprc1  3727  ruv  4583  xpindi  4798  xpindir  4799  dmcnvcnv  4887  rncnvcnv  4888  imainrect  5112  dfrn4  5127  fcoi1  5435  foimacnv  5519  fsnunfv  5760  dfoprab3  6246  fiintim  6987  sbthlemi8  7025  pitonnlem1  7907  ixi  8604  recexaplem2  8673  zeo  9425  num0h  9462  dec10p  9493  fseq1p1m1  10163  fsumrelem  11617  ef0lem  11806  ef01bndlem  11902  3lcm2e6woprm  12227  strsl0  12670  0g0  12962  tgioo  14733  tgqioo  14734  dveflem  14905  sincos4thpi  15016  coskpi  15024