Theorem 3eqtr3r 1504

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr3.1	|- A = B
3eqtr3.2	|- A = C
3eqtr3.3	|- B = D

Assertion

Ref	Expression
3eqtr3r	|- D = C

Proof of Theorem 3eqtr3r

Step	Hyp	Ref	Expression
1		3eqtr3.3	. 2 |- B = D
2		3eqtr3.1	. . 3 |- A = B
3		3eqtr3.2	. . 3 |- A = C
4	2, 3	eqtr3 1497	. 2 |- B = C
5	1, 4	eqtr3 1497	1 |- D = C

Syntax hints:   = wceq 956

This theorem is referenced by:  difdifdir 2346  cnvcnv 3486  resdm2 3496  co01 3509  dfdom2 4384  ixi 5681  discrlem1 6656  rei 6824  iserzshft 7144  fnsmnt 7226  cos1bnd 7474  cos2bnd 7475  ip1ilem 8485  minveclem38 8582  sinhalfpilem 8679  sincos4thpi 8710  sincos6thpi 8711  projlem18 9203  pjthlem14 9232  lnfn0 9971  pjclem1 10123  pjc 10128  mdexch 10262

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain