Theorem 3eqtr3rd 1519

Description: A deduction from three chained equalities.

Hypotheses

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

Assertion

Ref	Expression
3eqtr3rd	⊢ (φ → D = C)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (φ → B = D)
2		3eqtr3d.1	. . 3 ⊢ (φ → A = B)
3		3eqtr3d.2	. . 3 ⊢ (φ → A = C)
4	2, 3	eqtr3d 1512	. 2 ⊢ (φ → B = C)
5	1, 4	eqtr3d 1512	1 ⊢ (φ → D = C)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  subsub4t 5476  2halvest 6041  crrecz 6742  recjt 6818  bcnnt 6964  bcnp1nt 6966  ser1ser0 7048  serzmulc1 7057  iserzshft2 7107  georeclim 7240  sincossqt 7461  demoivreALT 7486  grpinvid1 8068  vcm 8186  ipasslem2 8487  minveclem35 8575  hosubsub4t 9739  lnop0t 9885  cnlnadjlem7 10001  adjbdlnb 10012  hst1ht 10149

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