Theorem eqtr2i 2253

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

Syntax hints:   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  3eqtrri  2257  3eqtr2ri  2259  symdif1  3472  dfif3  3619  dfsn2  3683  prprc1  3780  ruv  4648  xpindi  4865  xpindir  4866  dmcnvcnv  4956  rncnvcnv  4957  imainrect  5182  dfrn4  5197  fcoi1  5517  foimacnv  5601  fsnunfv  5855  dfoprab3  6354  fiintim  7123  sbthlemi8  7163  pitonnlem1  8065  ixi  8763  recexaplem2  8832  zeo  9585  num0h  9622  dec10p  9653  fseq1p1m1  10329  cats1fvn  11349  fsumrelem  12050  ef0lem  12239  ef01bndlem  12335  3lcm2e6woprm  12676  strsl0  13149  0g0  13477  tgioo  15297  tgqioo  15298  dveflem  15469  sincos4thpi  15583  coskpi  15591  0grsubgr  16134  konigsberglem5  16362  konigsberg  16363