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  4973  dmun  4988  resres  5075  inres  5080  resdifcom  5081  resiun1  5082  imainrect  5233  coundi  5289  coundir  5290  funopg  5411  offres  6368  mpomptsx  6433  cnvoprab  6470  snec  6870  halfpm6th  9530  numsucc  9826  decbin2  9927  fsumadd  12192  fsum2d  12221  fprodmul  12377  fprodfac  12401  fprodrec  12415  ballotfilemth  13333  znnen  13341  gsumfsum  15007  txswaphmeolem  15512  log2ublem3  16184  bposlem8  16279