Theorem eqtr2i 2229

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 2228	. 2 |- A = C
4	3	eqcomi 2211	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtrri  2233  3eqtr2ri  2235  symdif1  3446  dfif3  3593  dfsn2  3657  prprc1  3751  ruv  4616  xpindi  4831  xpindir  4832  dmcnvcnv  4921  rncnvcnv  4922  imainrect  5147  dfrn4  5162  fcoi1  5478  foimacnv  5562  fsnunfv  5808  dfoprab3  6300  fiintim  7054  sbthlemi8  7092  pitonnlem1  7993  ixi  8691  recexaplem2  8760  zeo  9513  num0h  9550  dec10p  9581  fseq1p1m1  10251  fsumrelem  11897  ef0lem  12086  ef01bndlem  12182  3lcm2e6woprm  12523  strsl0  12996  0g0  13323  tgioo  15141  tgqioo  15142  dveflem  15313  sincos4thpi  15427  coskpi  15435