Theorem 3eqtr2d 1516

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
3eqtr2d	|- (ph -> A = D)

Proof of Theorem 3eqtr2d

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

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  neg2subt 5471  binomlem5 7070  efi4pt 7435  addcost 7459  subcost 7460  sincossqt 7461  cos2tsint 7464  sin01bndlem3 7470  cos01bndlem3 7472  demoivre 7485  grpinvid2 8069  abldivdiv4 8105  vcoprne 8194  nvnncan 8279  sm1cnilem 8343  ipfval 8348  ipid 8359  ipasslem2 8487  shftefif1olem 8736  hv2timest 8923  pjds3 9653  ho2timest 9740  pjclem4 10122  pj3s 10130  csmdsym 10256  cmpmon 10714

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