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  8911  recexaplem2  8980  zeo  9751  num0h  9788  dec10p  9819  fseq1p1m1  10501  cats1fvn  11536  fsumrelem  12238  ef0lem  12427  ef01bndlem  12523  3lcm2e6woprm  12864  strsl0  13401  0g0  13696  isassa  15002  tgioo  15655  tgqioo  15656  dveflem  15827  sincos4thpi  15941  coskpi  15949  log2ublem1  16083  0grsubgr  16505  konigsberglem5  16733  konigsberg  16734