Theorem 3eqtr4ri 2263

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  cbvreucsf  3193  dfif6  3609  qdass  3772  tpidm12  3774  unipr  3912  dfdm4  4929  dmun  4944  resres  5031  inres  5036  resdifcom  5037  resiun1  5038  imainrect  5189  coundi  5245  coundir  5246  funopg  5367  offres  6306  mpomptsx  6371  cnvoprab  6408  snec  6808  halfpm6th  9423  numsucc  9711  decbin2  9812  fsumadd  12047  fsum2d  12076  fprodmul  12232  fprodfac  12256  fprodrec  12270  znnen  13099  txswaphmeolem  15131