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  3493  symdif1  3519  iunin  3547  iinun  3548  dfif3  3672  dfsn2  3747  ssunpr  3868  sstp  3870  tfinnn  4534  xpindi  4864  xpindir  4865  foimacnv  5303  clos1base  5878  pmex  6005  fundmen  6043  nncdiv3  6277  nnc3p1n3p2  6280  nchoicelem1  6289