Theorem 3eqtr4ri 2237

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  cbvreucsf  3158  dfif6  3573  qdass  3730  tpidm12  3732  unipr  3864  dfdm4  4871  dmun  4886  resres  4972  inres  4977  resdifcom  4978  resiun1  4979  imainrect  5129  coundi  5185  coundir  5186  funopg  5306  offres  6222  mpomptsx  6285  cnvoprab  6322  snec  6685  halfpm6th  9259  numsucc  9545  decbin2  9646  fsumadd  11750  fsum2d  11779  fprodmul  11935  fprodfac  11959  fprodrec  11973  znnen  12802  txswaphmeolem  14825