Theorem eqtr2i 2061

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

Syntax hints:   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtrri  2065  3eqtr2ri  2067  symdif1  3202  dfif3  3343  dfsn2  3389  prprc1  3478  ruv  4274  xpindi  4471  xpindir  4472  dmcnvcnv  4558  rncnvcnv  4559  imainrect  4766  dfrn4  4781  fcoi1  5070  foimacnv  5144  fsnunfv  5363  dfoprab3  5817  pitonnlem1  6921  ixi  7574  recexaplem2  7633  zeo  8343  num0h  8377  dec10p  8396  fseq1p1m1  8956