Theorem 3eqtr2rd 1514

Description: A deduction from three chained equalities.

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 |- (ph -> A = B)
2		3eqtr2d.2	. . 3 |- (ph -> C = B)
3	1, 2	eqtr4d 1510	. 2 |- (ph -> A = C)
4		3eqtr2d.3	. 2 |- (ph -> C = D)
5	3, 4	eqtr2d 1508	1 |- (ph -> D = A)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  recjt 6818  faclbnd2 6946  bcxmas 7076  geoser 7234  geoisum1c 7245  efsubt 7371  ef1tllem 7381  addsint 7457  subsint 7458  vc0 8188  ubthlem8 8536  adjco 10033  cnvbravalt 10043  mslb1 10629

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