Theorem 3eqtr2rd 1506

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

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  recjt 6753  faclbnd2 6883  bcxmas 7014  geoser 7169  geoisum1c 7180  efsubt 7313  ef1tllem 7323  addsint 7399  subsint 7400  vc0 8125  ubthlem8 8467  adjco 9947  cnvbravalt 9956  mslb1 10473

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