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  3424  dfif3  3570  dfsn2  3632  prprc1  3726  ruv  4582  xpindi  4797  xpindir  4798  dmcnvcnv  4886  rncnvcnv  4887  imainrect  5111  dfrn4  5126  fcoi1  5434  foimacnv  5518  fsnunfv  5759  dfoprab3  6244  fiintim  6985  sbthlemi8  7023  pitonnlem1  7905  ixi  8602  recexaplem2  8671  zeo  9422  num0h  9459  dec10p  9490  fseq1p1m1  10160  fsumrelem  11614  ef0lem  11803  ef01bndlem  11899  3lcm2e6woprm  12224  strsl0  12667  0g0  12959  tgioo  14714  tgqioo  14715  dveflem  14872  sincos4thpi  14975  coskpi  14983