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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtrri  2264  3eqtr2ri  2266  symdif1  3496  dfif3  3651  dfsn2  3719  prprc1  3816  ruv  4692  xpindi  4910  xpindir  4911  dmcnvcnv  5001  rncnvcnv  5002  imainrect  5228  dfrn4  5243  fcoi1  5567  foimacnv  5652  fsnunfv  5907  dfoprab3  6415  fiintim  7228  sbthlemi8  7271  pitonnlem1  8202  ixi  8901  recexaplem2  8970  zeo  9730  num0h  9767  dec10p  9798  fseq1p1m1  10479  cats1fvn  11514  fsumrelem  12216  ef0lem  12405  ef01bndlem  12501  3lcm2e6woprm  12842  strsl0  13379  0g0  13673  tgioo  15578  tgqioo  15579  dveflem  15750  sincos4thpi  15864  coskpi  15872  0grsubgr  16419  konigsberglem5  16647  konigsberg  16648