Theorem eqtr2i 2256

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  3eqtrri  2260  3eqtr2ri  2262  symdif1  3490  dfif3  3640  dfsn2  3708  prprc1  3805  ruv  4677  xpindi  4895  xpindir  4896  dmcnvcnv  4986  rncnvcnv  4987  imainrect  5213  dfrn4  5228  fcoi1  5552  foimacnv  5637  fsnunfv  5890  dfoprab3  6398  fiintim  7204  sbthlemi8  7247  pitonnlem1  8176  ixi  8874  recexaplem2  8943  zeo  9701  num0h  9738  dec10p  9769  fseq1p1m1  10450  cats1fvn  11481  fsumrelem  12182  ef0lem  12371  ef01bndlem  12467  3lcm2e6woprm  12808  strsl0  13345  0g0  13639  tgioo  15545  tgqioo  15546  dveflem  15717  sincos4thpi  15831  coskpi  15839  0grsubgr  16385  konigsberglem5  16613  konigsberg  16614