Theorem eqtr2i 2260

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 2259	. 2 |- A = C
4	3	eqcomi 2242	1 |- C = A

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  7242  sbthlemi8  7286  pitonnlem1  8218  ixi  8919  recexaplem2  8988  zeo  9762  num0h  9799  dec10p  9835  fseq1p1m1  10518  cats1fvn  11558  fsumrelem  12263  ef0lem  12452  ef01bndlem  12548  3lcm2e6woprm  12889  mod2xnegi  13227  strsl0  13459  0g0  13755  isassa  15111  tgioo  15780  tgqioo  15781  dveflem  15952  sincos4thpi  16067  coskpi  16075  log2ublem1  16221  bposlem9  16319  0grsubgr  16710  konigsberglem5  16938  konigsberg  16939