Theorem 3eqtr3g 2287

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3g.2	⊢ 𝐴 = 𝐶
3eqtr3g.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 ⊢ 𝐴 = 𝐶
2		3eqtr3g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr3id 2278	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2280	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  csbnest1g  3183  disjdif2  3573  dfopg  3860  xpid11  4955  sqxpeq0  5160  cores2  5249  funcoeqres  5614  dftpos2  6427  ine0  8573  fisumcom2  12017  fisum0diag2  12026  mertenslemi1  12114  fprodcom2fi  12205  fprodmodd  12220  bitsinv1  12541  4sqlem10  12978  setsslnid  13152  xpsff1o  13450  eqglact  13830  oppr1g  14114  dvmptccn  15458  dvmptc  15460  dvmptfsum  15468  fsumdvdsmul  15734  nninffeq  16673