Theorem eqtr2i 2253

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)

Hypotheses

Ref	Expression
eqtr2i.1	|- A = B
eqtr2i.2	|- B = C

Assertion

Ref	Expression
eqtr2i	|- C = A

Proof of Theorem eqtr2i

Step	Hyp	Ref	Expression
1		eqtr2i.1	. . 3 |- A = B
2		eqtr2i.2	. . 3 |- B = C
3	1, 2	eqtri 2252	. 2 |- A = C
4	3	eqcomi 2235	1 |- C = A

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtrri  2257  3eqtr2ri  2259  symdif1  3474  dfif3  3623  dfsn2  3687  prprc1  3784  ruv  4654  xpindi  4871  xpindir  4872  dmcnvcnv  4962  rncnvcnv  4963  imainrect  5189  dfrn4  5204  fcoi1  5525  foimacnv  5610  fsnunfv  5863  dfoprab3  6363  fiintim  7166  sbthlemi8  7206  pitonnlem1  8125  ixi  8822  recexaplem2  8891  zeo  9646  num0h  9683  dec10p  9714  fseq1p1m1  10391  cats1fvn  11411  fsumrelem  12112  ef0lem  12301  ef01bndlem  12397  3lcm2e6woprm  12738  strsl0  13211  0g0  13539  tgioo  15365  tgqioo  15366  dveflem  15537  sincos4thpi  15651  coskpi  15659  0grsubgr  16205  konigsberglem5  16433  konigsberg  16434