Theorem 3eqtr3g 1146

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

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.1	. . 3 ⊢ (φ → A = B)
2		3eqtr3g.2	. . 3 ⊢ A = C
3	1, 2	syl5eqr 1138	. 2 ⊢ (φ → C = B)
4		3eqtr3g.3	. 2 ⊢ B = D
5	3, 4	syl6eq 1140	1 ⊢ (φ → C = D)

Syntax hints:   → wi 2   = wceq 1091

This theorem is referenced by:  opprc2 1907  aceq5lem3 3560  reclem3pr 3952  mulcmpblnrlem 3976  1idsr 4001  mulgt0sr 4008  subeq0 4163  ine0 4524  crulem 4528  discrlem3 4715  ruclem18 4902  ruclem19 4903  ruclem20 4904  ruclem21 4905  hvsubeq0 5035  hvaddcan 5037  cmcmlem 5500  pj11 5591  pjclem1 5649  pjclem3 5651  st0 5690  mdsym 5784

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