Theorem eqtr2i 2199

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtrri  2203  3eqtr2ri  2205  symdif1  3401  dfif3  3548  dfsn2  3607  prprc1  3701  ruv  4550  xpindi  4763  xpindir  4764  dmcnvcnv  4852  rncnvcnv  4853  imainrect  5075  dfrn4  5090  fcoi1  5397  foimacnv  5480  fsnunfv  5718  dfoprab3  6192  fiintim  6928  sbthlemi8  6963  pitonnlem1  7844  ixi  8540  recexaplem2  8609  zeo  9358  num0h  9395  dec10p  9426  fseq1p1m1  10094  fsumrelem  11479  ef0lem  11668  ef01bndlem  11764  3lcm2e6woprm  12086  strsl0  12511  0g0  12795  tgioo  14049  tgqioo  14050  dveflem  14190  sincos4thpi  14264  coskpi  14272