Theorem eqtr2i 2110

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

Syntax hints:   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

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

This theorem is referenced by:  3eqtrri  2114  3eqtr2ri  2116  symdif1  3265  dfif3  3410  dfsn2  3464  prprc1  3554  ruv  4379  xpindi  4584  xpindir  4585  dmcnvcnv  4672  rncnvcnv  4673  imainrect  4889  dfrn4  4904  fcoi1  5204  foimacnv  5284  fsnunfv  5512  dfoprab3  5975  fiintim  6693  sbthlemi8  6727  pitonnlem1  7436  ixi  8114  recexaplem2  8175  zeo  8905  num0h  8942  dec10p  8973  fseq1p1m1  9562  fsumrelem  10919  ef0lem  11004  ef01bndlem  11101  3lcm2e6woprm  11400  strsl0  11596