Theorem 3eqtr3rd 1513

Description: A deduction from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtr3rd	|- (ph -> D = C)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 |- (ph -> B = D)
2		3eqtr3d.1	. . 3 |- (ph -> A = B)
3		3eqtr3d.2	. . 3 |- (ph -> A = C)
4	2, 3	eqtr3d 1506	. 2 |- (ph -> B = C)
5	1, 4	eqtr3d 1506	1 |- (ph -> D = C)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  subsub4t 5444  2halvest 5994  crrecz 6680  recjt 6761  bcnnt 6910  bcnp1nt 6912  ser1ser0 6994  serzmulc1 7003  iserzshft2 7052  georeclim 7183  sincossqt 7411  demoivreALT 7435  grpinvid1 8022  vcm 8142  ipasslem2 8435  minveclem35 8523  hosubsub4t 9684  lnop0t 9829  cnlnadjlem7 9944  adjbdlnb 9955  hst1ht 10092

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

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

Copyright terms: Public domain