Theorem 3eqtr3d 1133

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
3eqtr3d	|- (ph -> C = D)

Proof of Theorem 3eqtr3d

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

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  f1ocnvfv1 2919  f1ocnvfv2 2920  mapenlem1 3384  mapenlem2 3385  phplem5 3407  php3 3411  cardiun 3665  add12t 4125  add4t 4127  mul4t 4177  divadddivt 4264  divdivdivt 4265  recdivt 4270  uzind 4603  sqr11 4761  facnnt 4870  hvadd12t 5012  hvadd4t 5013  h1de2b 5459  spanunsn 5482  5oalem2 5545  3oalem2 5553  strlem1 5691

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org