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  8212  ixi  8913  recexaplem2  8982  zeo  9755  num0h  9792  dec10p  9828  fseq1p1m1  10511  cats1fvn  11550  fsumrelem  12254  ef0lem  12443  ef01bndlem  12539  3lcm2e6woprm  12880  mod2xnegi  13218  strsl0  13450  0g0  13745  isassa  15051  tgioo  15704  tgqioo  15705  dveflem  15876  sincos4thpi  15991  coskpi  15999  log2ublem1  16140  0grsubgr  16603  konigsberglem5  16831  konigsberg  16832