Theorem 3eqtr4ri 2209

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  cbvreucsf  3121  dfif6  3536  qdass  3689  tpidm12  3691  unipr  3822  dfdm4  4816  dmun  4831  resres  4916  inres  4921  resdifcom  4922  resiun1  4923  imainrect  5071  coundi  5127  coundir  5128  funopg  5247  offres  6131  mpomptsx  6193  cnvoprab  6230  snec  6591  halfpm6th  9133  numsucc  9417  decbin2  9518  fsumadd  11405  fsum2d  11434  fprodmul  11590  fprodfac  11614  fprodrec  11628  znnen  12389