Theorem 3eqtr4ri 2228

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 2220	. 2 |- D = A
4		3eqtr4i.2	. 2 |- C = A
5	3, 4	eqtr4i 2220	1 |- D = C

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  cbvreucsf  3149  dfif6  3564  qdass  3720  tpidm12  3722  unipr  3854  dfdm4  4859  dmun  4874  resres  4959  inres  4964  resdifcom  4965  resiun1  4966  imainrect  5116  coundi  5172  coundir  5173  funopg  5293  offres  6201  mpomptsx  6264  cnvoprab  6301  snec  6664  halfpm6th  9228  numsucc  9513  decbin2  9614  fsumadd  11588  fsum2d  11617  fprodmul  11773  fprodfac  11797  fprodrec  11811  znnen  12640  txswaphmeolem  14640