Theorem 3eqtrrd 1504

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 1500	. 2 |- (ph -> C = A)
5	1, 4	eqtr3d 1501	1 |- (ph -> D = A)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  axcnre 5258  seq1seq02t 6475  seqzp1 6480  expubndt 6539  subsqt 6573  sincossqt 7403  nmbdoplb 9864  nmcopexlem3 9868  nmcoplb 9873  nmbdfnlb 9893  nmcfnexlem3 9897  nmcfnlb 9902  hstoht 10069

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain