Theorem eqtr2i 2228

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

Syntax hints:   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199

This theorem is referenced by:  3eqtrri  2232  3eqtr2ri  2234  symdif1  3442  dfif3  3589  dfsn2  3652  prprc1  3746  ruv  4606  xpindi  4821  xpindir  4822  dmcnvcnv  4911  rncnvcnv  4912  imainrect  5137  dfrn4  5152  fcoi1  5468  foimacnv  5552  fsnunfv  5798  dfoprab3  6290  fiintim  7043  sbthlemi8  7081  pitonnlem1  7978  ixi  8676  recexaplem2  8745  zeo  9498  num0h  9535  dec10p  9566  fseq1p1m1  10236  fsumrelem  11857  ef0lem  12046  ef01bndlem  12142  3lcm2e6woprm  12483  strsl0  12956  0g0  13283  tgioo  15101  tgqioo  15102  dveflem  15273  sincos4thpi  15387  coskpi  15395