Theorem eqtr2i 2179

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

Syntax hints:   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  3eqtrri  2183  3eqtr2ri  2185  symdif1  3372  dfif3  3518  dfsn2  3574  prprc1  3667  ruv  4508  xpindi  4720  xpindir  4721  dmcnvcnv  4809  rncnvcnv  4810  imainrect  5030  dfrn4  5045  fcoi1  5349  foimacnv  5431  fsnunfv  5667  dfoprab3  6136  fiintim  6870  sbthlemi8  6905  pitonnlem1  7759  ixi  8452  recexaplem2  8520  zeo  9263  num0h  9300  dec10p  9331  fseq1p1m1  9989  fsumrelem  11361  ef0lem  11550  ef01bndlem  11646  3lcm2e6woprm  11954  strsl0  12209  tgioo  12917  tgqioo  12918  dveflem  13058  sincos4thpi  13132  coskpi  13140