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  4598  xpindi  4813  xpindir  4814  dmcnvcnv  4902  rncnvcnv  4903  imainrect  5128  dfrn4  5143  fcoi1  5456  foimacnv  5540  fsnunfv  5785  dfoprab3  6277  fiintim  7028  sbthlemi8  7066  pitonnlem1  7958  ixi  8656  recexaplem2  8725  zeo  9478  num0h  9515  dec10p  9546  fseq1p1m1  10216  fsumrelem  11782  ef0lem  11971  ef01bndlem  12067  3lcm2e6woprm  12408  strsl0  12881  0g0  13208  tgioo  15026  tgqioo  15027  dveflem  15198  sincos4thpi  15312  coskpi  15320