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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  csbnest1g  3184  disjdif2  3575  dfopg  3865  xpid11  4961  sqxpeq0  5167  cores2  5256  funcoeqres  5623  dftpos2  6470  ine0  8615  fisumcom2  12062  fisum0diag2  12071  mertenslemi1  12159  fprodcom2fi  12250  fprodmodd  12265  bitsinv1  12586  4sqlem10  13023  setsslnid  13197  xpsff1o  13495  eqglact  13875  oppr1g  14159  dvmptccn  15509  dvmptc  15511  dvmptfsum  15519  fsumdvdsmul  15788  nninffeq  16729