Theorem 3eqtr4ri 2197

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

Syntax hints:   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  cbvreucsf  3109  dfif6  3522  qdass  3673  tpidm12  3675  unipr  3803  dfdm4  4796  dmun  4811  resres  4896  inres  4901  resdifcom  4902  resiun1  4903  imainrect  5049  coundi  5105  coundir  5106  funopg  5222  offres  6103  mpomptsx  6165  cnvoprab  6202  snec  6562  halfpm6th  9077  numsucc  9361  decbin2  9462  fsumadd  11347  fsum2d  11376  fprodmul  11532  fprodfac  11556  fprodrec  11570  znnen  12331