Theorem eqtr2i 2374

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

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  3eqtrri  2378  3eqtr2ri  2380  dfun3  3494  symdif1  3520  iunin  3548  iinun  3549  dfif3  3673  dfsn2  3748  ssunpr  3869  sstp  3871  tfinnn  4535  xpindi  4865  xpindir  4866  foimacnv  5304  clos1base  5879  pmex  6006  fundmen  6044  nncdiv3  6278  nnc3p1n3p2  6281  nchoicelem1  6290