Theorem eqtr2i 2253

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtrri  2257  3eqtr2ri  2259  symdif1  3472  dfif3  3619  dfsn2  3683  prprc1  3780  ruv  4648  xpindi  4865  xpindir  4866  dmcnvcnv  4956  rncnvcnv  4957  imainrect  5182  dfrn4  5197  fcoi1  5517  foimacnv  5601  fsnunfv  5854  dfoprab3  6353  fiintim  7122  sbthlemi8  7162  pitonnlem1  8064  ixi  8762  recexaplem2  8831  zeo  9584  num0h  9621  dec10p  9652  fseq1p1m1  10328  cats1fvn  11344  fsumrelem  12031  ef0lem  12220  ef01bndlem  12316  3lcm2e6woprm  12657  strsl0  13130  0g0  13458  tgioo  15277  tgqioo  15278  dveflem  15449  sincos4thpi  15563  coskpi  15571  0grsubgr  16114