Theorem 3eqtr4ri 2270

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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  cbvreucsf  3212  dfif6  3637  qdass  3804  tpidm12  3806  unipr  3944  dfdm4  4968  dmun  4983  resres  5070  inres  5075  resdifcom  5076  resiun1  5077  imainrect  5228  coundi  5284  coundir  5285  funopg  5406  offres  6358  mpomptsx  6423  cnvoprab  6460  snec  6860  halfpm6th  9504  numsucc  9795  decbin2  9896  fsumadd  12151  fsum2d  12180  fprodmul  12336  fprodfac  12360  fprodrec  12374  ballotfilemth  13259  znnen  13267  gsumfsum  14895  txswaphmeolem  15344