Theorem 3eqtr3rd 1516

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 1509	. 2 |- (ph -> B = C)
5	1, 4	eqtr3d 1509	1 |- (ph -> D = C)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  subsub4t 5464  2halvest 6039  crrecz 6741  recjt 6818  bcnnt 6964  bcnp1nt 6966  ser1ser0 7048  serzmulc1 7057  iserzshft2 7107  georeclim 7240  sincossqt 7461  demoivreALT 7485  grpinvid1 8072  vcm 8190  ipasslem2 8491  minveclem35 8579  hosubsub4t 9744  lnop0t 9890  cnlnadjlem7 10006  adjbdlnb 10017  hst1ht 10154

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