Theorem eqtr2i 2218

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtrri  2222  3eqtr2ri  2224  symdif1  3429  dfif3  3575  dfsn2  3637  prprc1  3731  ruv  4587  xpindi  4802  xpindir  4803  dmcnvcnv  4891  rncnvcnv  4892  imainrect  5116  dfrn4  5131  fcoi1  5441  foimacnv  5525  fsnunfv  5766  dfoprab3  6258  fiintim  7001  sbthlemi8  7039  pitonnlem1  7929  ixi  8627  recexaplem2  8696  zeo  9448  num0h  9485  dec10p  9516  fseq1p1m1  10186  fsumrelem  11653  ef0lem  11842  ef01bndlem  11938  3lcm2e6woprm  12279  strsl0  12752  0g0  13078  tgioo  14874  tgqioo  14875  dveflem  15046  sincos4thpi  15160  coskpi  15168