Theorem 3eqtr3g 2252

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  csbnest1g  3140  disjdif2  3530  dfopg  3807  xpid11  4890  sqxpeq0  5094  cores2  5183  funcoeqres  5536  dftpos2  6321  ine0  8423  fisumcom2  11606  fisum0diag2  11615  mertenslemi1  11703  fprodcom2fi  11794  fprodmodd  11809  bitsinv1  12130  4sqlem10  12567  setsslnid  12741  xpsff1o  13018  eqglact  13381  oppr1g  13664  dvmptccn  14977  dvmptc  14979  dvmptfsum  14987  fsumdvdsmul  15253  nninffeq  15693