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  6426  ine0  8572  fisumcom2  11998  fisum0diag2  12007  mertenslemi1  12095  fprodcom2fi  12186  fprodmodd  12201  bitsinv1  12522  4sqlem10  12959  setsslnid  13133  xpsff1o  13431  eqglact  13811  oppr1g  14094  dvmptccn  15438  dvmptc  15440  dvmptfsum  15448  fsumdvdsmul  15714  nninffeq  16622