Theorem eqtr2i 2192

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

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  3eqtrri  2196  3eqtr2ri  2198  symdif1  3392  dfif3  3539  dfsn2  3597  prprc1  3691  ruv  4534  xpindi  4746  xpindir  4747  dmcnvcnv  4835  rncnvcnv  4836  imainrect  5056  dfrn4  5071  fcoi1  5378  foimacnv  5460  fsnunfv  5697  dfoprab3  6170  fiintim  6906  sbthlemi8  6941  pitonnlem1  7807  ixi  8502  recexaplem2  8570  zeo  9317  num0h  9354  dec10p  9385  fseq1p1m1  10050  fsumrelem  11434  ef0lem  11623  ef01bndlem  11719  3lcm2e6woprm  12040  strsl0  12464  0g0  12630  tgioo  13340  tgqioo  13341  dveflem  13481  sincos4thpi  13555  coskpi  13563