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  4697  xpindi  4915  xpindir  4916  dmcnvcnv  5006  rncnvcnv  5007  imainrect  5233  dfrn4  5248  fcoi1  5572  foimacnv  5657  fsnunfv  5916  dfoprab3  6425  fiintim  7238  sbthlemi8  7281  pitonnlem1  8213  ixi  8914  recexaplem2  8983  zeo  9756  num0h  9793  dec10p  9829  fseq1p1m1  10512  cats1fvn  11552  fsumrelem  12257  ef0lem  12446  ef01bndlem  12542  3lcm2e6woprm  12883  mod2xnegi  13221  strsl0  13453  0g0  13749  isassa  15086  tgioo  15746  tgqioo  15747  dveflem  15918  sincos4thpi  16033  coskpi  16041  log2ublem1  16182  bposlem9  16280  0grsubgr  16671  konigsberglem5  16899  konigsberg  16900