Theorem 3eqtr4ri 2202

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

Syntax hints:   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  cbvreucsf  3113  dfif6  3528  qdass  3680  tpidm12  3682  unipr  3810  dfdm4  4803  dmun  4818  resres  4903  inres  4908  resdifcom  4909  resiun1  4910  imainrect  5056  coundi  5112  coundir  5113  funopg  5232  offres  6114  mpomptsx  6176  cnvoprab  6213  snec  6574  halfpm6th  9098  numsucc  9382  decbin2  9483  fsumadd  11369  fsum2d  11398  fprodmul  11554  fprodfac  11578  fprodrec  11592  znnen  12353