Theorem 3eqtr3g 1529

Description: A chained equality inference, useful for converting from definitions.

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.1	. . 3 |- (ph -> A = B)
2		3eqtr3g.2	. . 3 |- A = C
3	1, 2	syl5eqr 1520	. 2 |- (ph -> C = B)
4		3eqtr3g.3	. 2 |- B = D
5	3, 4	syl6eq 1522	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 955

This theorem is referenced by:  abidhb 1910  hbsbc1gd 1981  hbsbcgd 1982  opprc2 2497  onnev 3239  xpid11 3332  cores2 3504  oev2 4159  aceq5lem3 4724  reclem3pr 5145  mulcmpblnrlem 5169  1idsr 5194  mulgt0sr 5201  ine0 5421  discrlem3 6608  crulem 6687  ruclem18 7506  ruclem19 7507  ruclem20 7508  ruclem21 7509  pythi 8494  hvsubeq0 8914  hvaddcan 8916  cmcmlem 9524  pj11 9647  hosubeq0 9743  riesz3 9986  pjclem1 10114  pjclem3 10116  st0 10167  irred 10312  mdsym 10329  trnij 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

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

Copyright terms: Public domain