Theorem eqtr2i 2254

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 2253	. 2 |- A = C
4	3	eqcomi 2236	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 2214

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

This theorem is referenced by:  3eqtrri  2258  3eqtr2ri  2260  symdif1  3486  dfif3  3636  dfsn2  3703  prprc1  3800  ruv  4672  xpindi  4890  xpindir  4891  dmcnvcnv  4981  rncnvcnv  4982  imainrect  5208  dfrn4  5223  fcoi1  5547  foimacnv  5632  fsnunfv  5885  dfoprab3  6385  fiintim  7191  sbthlemi8  7234  pitonnlem1  8160  ixi  8857  recexaplem2  8926  zeo  9683  num0h  9720  dec10p  9751  fseq1p1m1  10428  cats1fvn  11456  fsumrelem  12157  ef0lem  12346  ef01bndlem  12442  3lcm2e6woprm  12783  strsl0  13261  0g0  13589  tgioo  15419  tgqioo  15420  dveflem  15591  sincos4thpi  15705  coskpi  15713  0grsubgr  16259  konigsberglem5  16487  konigsberg  16488