Theorem eqtr2i 2260

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtrri  2264  3eqtr2ri  2266  symdif1  3496  dfif3  3654  dfsn2  3723  prprc1  3821  ruv  4699  xpindi  4917  xpindir  4918  dmcnvcnv  5008  rncnvcnv  5009  imainrect  5236  dfrn4  5251  fcoi1  5575  foimacnv  5660  fsnunfv  5919  dfoprab3  6429  fiintim  7244  sbthlemi8  7288  pitonnlem1  8218  ixi  8919  recexaplem2  8988  zeo  9761  num0h  9798  dec10p  9834  fseq1p1m1  10517  cats1fvn  11557  fsumrelem  12262  ef0lem  12451  ef01bndlem  12547  3lcm2e6woprm  12888  mod2xnegi  13226  strsl0  13458  0g0  13754  isassa  15110  tgioo  15797  tgqioo  15798  dveflem  15969  sincos4thpi  16084  coskpi  16092  log2ublem1  16238  bposlem9  16336  0grsubgr  16727  konigsberglem5  16955  konigsberg  16956