Theorem eqtr2i 2162

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

Syntax hints:   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  3eqtrri  2166  3eqtr2ri  2168  symdif1  3346  dfif3  3492  dfsn2  3546  prprc1  3639  ruv  4473  xpindi  4682  xpindir  4683  dmcnvcnv  4771  rncnvcnv  4772  imainrect  4992  dfrn4  5007  fcoi1  5311  foimacnv  5393  fsnunfv  5629  dfoprab3  6097  fiintim  6825  sbthlemi8  6860  pitonnlem1  7677  ixi  8369  recexaplem2  8437  zeo  9180  num0h  9217  dec10p  9248  fseq1p1m1  9905  fsumrelem  11272  ef0lem  11403  ef01bndlem  11499  3lcm2e6woprm  11803  strsl0  12046  tgioo  12754  tgqioo  12755  dveflem  12895  sincos4thpi  12969  coskpi  12977