Theorem 3eqtr4ri 2239

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  cbvreucsf  3166  dfif6  3581  qdass  3740  tpidm12  3742  unipr  3878  dfdm4  4889  dmun  4904  resres  4990  inres  4995  resdifcom  4996  resiun1  4997  imainrect  5147  coundi  5203  coundir  5204  funopg  5324  offres  6243  mpomptsx  6306  cnvoprab  6343  snec  6706  halfpm6th  9292  numsucc  9578  decbin2  9679  fsumadd  11832  fsum2d  11861  fprodmul  12017  fprodfac  12041  fprodrec  12055  znnen  12884  txswaphmeolem  14907