Theorem eqtr2i 2187

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtrri  2191  3eqtr2ri  2193  symdif1  3387  dfif3  3533  dfsn2  3590  prprc1  3684  ruv  4527  xpindi  4739  xpindir  4740  dmcnvcnv  4828  rncnvcnv  4829  imainrect  5049  dfrn4  5064  fcoi1  5368  foimacnv  5450  fsnunfv  5686  dfoprab3  6159  fiintim  6894  sbthlemi8  6929  pitonnlem1  7786  ixi  8481  recexaplem2  8549  zeo  9296  num0h  9333  dec10p  9364  fseq1p1m1  10029  fsumrelem  11412  ef0lem  11601  ef01bndlem  11697  3lcm2e6woprm  12018  strsl0  12442  0g0  12607  tgioo  13196  tgqioo  13197  dveflem  13337  sincos4thpi  13411  coskpi  13419