Theorem 3eqtr3g 2288

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 2279	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2281	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 2214

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

This theorem is referenced by:  csbnest1g  3194  disjdif2  3588  dfopg  3881  xpid11  4980  sqxpeq0  5186  cores2  5275  funcoeqres  5645  dftpos2  6492  ine0  8667  fisumcom2  12124  fisum0diag2  12133  mertenslemi1  12221  fprodcom2fi  12312  fprodmodd  12327  bitsinv1  12648  4sqlem10  13085  setsslnid  13264  xpsff1o  13562  eqglact  13942  oppr1g  14226  dvmptccn  15580  dvmptc  15582  dvmptfsum  15590  fsumdvdsmul  15859  nninffeq  16798