Theorem 3eqtr2d 1513

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  neg2subt 5459  binomlem5 7070  efi4pt 7435  addcost 7459  subcost 7460  sincossqt 7461  sin01bndlem3 7469  cos01bndlem3 7471  demoivre 7484  grpinvid2 8073  abldivdiv4 8109  vcoprne 8198  nvnncan 8283  sm1cnilem 8347  ipfval 8352  ipid 8363  ipasslem2 8491  shftefif1olem 8741  hv2timest 8928  pjds3 9658  ho2timest 9745  pjclem4 10127  pj3s 10135  csmdsym 10261  cmpmon 10743

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