Theorem 3eqtr4ri 2264

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr4i.1	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4ri	|- D = C

Proof of Theorem 3eqtr4ri

Step	Hyp	Ref	Expression
1		3eqtr4i.3	. . 3 |- D = B
2		3eqtr4i.1	. . 3 |- A = B
3	1, 2	eqtr4i 2256	. 2 |- D = A
4		3eqtr4i.2	. 2 |- C = A
5	3, 4	eqtr4i 2256	1 |- D = C

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 2214

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

This theorem is referenced by:  cbvreucsf  3203  dfif6  3622  qdass  3788  tpidm12  3790  unipr  3928  dfdm4  4948  dmun  4963  resres  5050  inres  5055  resdifcom  5056  resiun1  5057  imainrect  5208  coundi  5264  coundir  5265  funopg  5386  offres  6328  mpomptsx  6393  cnvoprab  6430  snec  6830  halfpm6th  9458  numsucc  9748  decbin2  9849  fsumadd  12092  fsum2d  12121  fprodmul  12277  fprodfac  12301  fprodrec  12315  znnen  13149  txswaphmeolem  15185