Theorem eqtr2i 2161

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 2160	. 2 |- A = C
4	3	eqcomi 2143	1 |- C = A

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  3eqtrri  2165  3eqtr2ri  2167  symdif1  3341  dfif3  3487  dfsn2  3541  prprc1  3631  ruv  4465  xpindi  4674  xpindir  4675  dmcnvcnv  4763  rncnvcnv  4764  imainrect  4984  dfrn4  4999  fcoi1  5303  foimacnv  5385  fsnunfv  5621  dfoprab3  6089  fiintim  6817  sbthlemi8  6852  pitonnlem1  7653  ixi  8345  recexaplem2  8413  zeo  9156  num0h  9193  dec10p  9224  fseq1p1m1  9874  fsumrelem  11240  ef0lem  11366  ef01bndlem  11463  3lcm2e6woprm  11767  strsl0  12007  tgioo  12715  tgqioo  12716  dveflem  12855  sincos4thpi  12921  coskpi  12929