Theorem eqtr2i 2102

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)

Hypotheses

Ref	Expression
eqtr2i.1	⊢ 𝐴 = 𝐵
eqtr2i.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtr2i	⊢ 𝐶 = 𝐴

Proof of Theorem eqtr2i

Step	Hyp	Ref	Expression
1		eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2i.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtri 2101	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2085	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtrri  2106  3eqtr2ri  2108  symdif1  3229  dfif3  3364  dfsn2  3412  prprc1  3500  ruv  4293  xpindi  4489  xpindir  4490  dmcnvcnv  4576  rncnvcnv  4577  imainrect  4786  dfrn4  4801  fcoi1  5090  foimacnv  5164  fsnunfv  5384  dfoprab3  5837  pitonnlem1  7013  ixi  7683  recexaplem2  7742  zeo  8452  num0h  8488  dec10p  8519  fseq1p1m1  9111  3lcm2e6woprm  10468