Theorem eqtr2i 2227

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtrri  2231  3eqtr2ri  2233  symdif1  3438  dfif3  3584  dfsn2  3647  prprc1  3741  ruv  4599  xpindi  4814  xpindir  4815  dmcnvcnv  4903  rncnvcnv  4904  imainrect  5129  dfrn4  5144  fcoi1  5458  foimacnv  5542  fsnunfv  5787  dfoprab3  6279  fiintim  7030  sbthlemi8  7068  pitonnlem1  7960  ixi  8658  recexaplem2  8727  zeo  9480  num0h  9517  dec10p  9548  fseq1p1m1  10218  fsumrelem  11815  ef0lem  12004  ef01bndlem  12100  3lcm2e6woprm  12441  strsl0  12914  0g0  13241  tgioo  15059  tgqioo  15060  dveflem  15231  sincos4thpi  15345  coskpi  15353