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  3563  qdass  3719  tpidm12  3721  unipr  3853  dfdm4  4858  dmun  4873  resres  4958  inres  4963  resdifcom  4964  resiun1  4965  imainrect  5115  coundi  5171  coundir  5172  funopg  5292  offres  6192  mpomptsx  6255  cnvoprab  6292  snec  6655  halfpm6th  9211  numsucc  9496  decbin2  9597  fsumadd  11571  fsum2d  11600  fprodmul  11756  fprodfac  11780  fprodrec  11794  znnen  12615  txswaphmeolem  14556