Theorem eqtr2i 2103

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 2102	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2086	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1285

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

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

This theorem is referenced by:  3eqtrri  2107  3eqtr2ri  2109  symdif1  3236  dfif3  3372  dfsn2  3420  prprc1  3508  ruv  4301  xpindi  4499  xpindir  4500  dmcnvcnv  4586  rncnvcnv  4587  imainrect  4796  dfrn4  4811  fcoi1  5101  foimacnv  5175  fsnunfv  5395  dfoprab3  5848  pitonnlem1  7075  ixi  7750  recexaplem2  7809  zeo  8533  num0h  8569  dec10p  8600  fseq1p1m1  9187  3lcm2e6woprm  10612