Theorem 3eqtr4ri 2225

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 2217	. 2 |- D = A
4		3eqtr4i.2	. 2 |- C = A
5	3, 4	eqtr4i 2217	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  cbvreucsf  3145  dfif6  3559  qdass  3715  tpidm12  3717  unipr  3849  dfdm4  4854  dmun  4869  resres  4954  inres  4959  resdifcom  4960  resiun1  4961  imainrect  5111  coundi  5167  coundir  5168  funopg  5288  offres  6187  mpomptsx  6250  cnvoprab  6287  snec  6650  halfpm6th  9202  numsucc  9487  decbin2  9588  fsumadd  11549  fsum2d  11578  fprodmul  11734  fprodfac  11758  fprodrec  11772  znnen  12555  txswaphmeolem  14488