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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cbvreucsf  3212  dfif6  3640  qdass  3808  tpidm12  3810  unipr  3949  dfdm4  4975  dmun  4990  resres  5077  inres  5082  resdifcom  5083  resiun1  5084  imainrect  5236  coundi  5292  coundir  5293  funopg  5414  offres  6372  mpomptsx  6437  cnvoprab  6474  snec  6875  halfpm6th  9536  numsucc  9831  decbin2  9932  fsumadd  12197  fsum2d  12226  fprodmul  12382  fprodfac  12406  fprodrec  12420  ballotfilemth  13338  znnen  13346  gsumfsum  15031  txswaphmeolem  15563  log2ublem3  16240  bposlem8  16335