Theorem 3eqtr3g 1533

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 1524	. 2 |- (ph -> C = B)
4		3eqtr3g.3	. 2 |- B = D
5	3, 4	syl6eq 1526	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  abidhb 1915  hbsbc1gd 1986  hbsbcgd 1987  opprc2 2503  onnev 3248  xpid11 3341  cores2 3513  oev2 4168  aceq5lem3 4747  reclem3pr 5170  mulcmpblnrlem 5194  1idsr 5219  mulgt0sr 5226  ine0 5446  discrlem3 6659  crulem 6737  ruclem18 7528  ruclem19 7529  ruclem20 7530  ruclem21 7531  pythi 8506  hvsubeq0 8925  hvaddcan 8927  cmcmlem 9529  pj11 9651  hosubeq0 9747  riesz3 9990  pjclem1 10118  pjclem3 10120  st0 10171  irred 10316  mdsym 10333  trnij 10608

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