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  3400  dfif3  3547  dfsn2  3606  prprc1  3700  ruv  4549  xpindi  4762  xpindir  4763  dmcnvcnv  4851  rncnvcnv  4852  imainrect  5074  dfrn4  5089  fcoi1  5396  foimacnv  5479  fsnunfv  5717  dfoprab3  6191  fiintim  6927  sbthlemi8  6962  pitonnlem1  7843  ixi  8538  recexaplem2  8607  zeo  9356  num0h  9393  dec10p  9424  fseq1p1m1  10091  fsumrelem  11474  ef0lem  11663  ef01bndlem  11759  3lcm2e6woprm  12080  strsl0  12505  0g0  12789  tgioo  13977  tgqioo  13978  dveflem  14118  sincos4thpi  14192  coskpi  14200