Theorem 3eqtrrd 1559

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtrd.1	|- (ph -> A = B)
3eqtrd.2	|- (ph -> B = C)
3eqtrd.3	|- (ph -> C = D)

Assertion

Ref	Expression
3eqtrrd	|- (ph -> D = A)

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.3	. 2 |- (ph -> C = D)
2		3eqtrd.1	. . 3 |- (ph -> A = B)
3		3eqtrd.2	. . 3 |- (ph -> B = C)
4	2, 3	eqtr2d 1555	. 2 |- (ph -> C = A)
5	1, 4	eqtr3d 1556	1 |- (ph -> D = A)

Syntax hints:   -> wi 3   = wceq 997

This theorem is referenced by:  axcnre 5351  flmodOLD 6375  seq1seq02 6632  seqzp1 6637  expubnd 6697  subsq 6731  rereb 6866  sincossq 7552  abssinper 8795  nmbdoplbi 10032  nmcopexlem3 10036  nmcoplbi 10041  nmbdfnlbi 10061  nmcfnexlem3 10065  nmcfnlbi 10070  hstoh 10243

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain