Theorem 3eqtr2rd 1517

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (φ → A = B)
3eqtr2d.2	⊢ (φ → C = B)
3eqtr2d.3	⊢ (φ → C = D)

Assertion

Ref	Expression
3eqtr2rd	⊢ (φ → D = A)

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (φ → A = B)
2		3eqtr2d.2	. . 3 ⊢ (φ → C = B)
3	1, 2	eqtr4d 1513	. 2 ⊢ (φ → A = C)
4		3eqtr2d.3	. 2 ⊢ (φ → C = D)
5	3, 4	eqtr2d 1511	1 ⊢ (φ → D = A)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  recjt 6818  faclbnd2 6946  bcxmas 7076  geoser 7234  geoisum1c 7245  efsubt 7371  ef1tllem 7381  addsint 7457  subsint 7458  vc0 8184  ubthlem8 8532  adjco 10028  cnvbravalt 10038  mslb1 10600

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain