Theorem 3eqtr3g 2294

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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  csbnest1g  3203  disjdif2  3603  dfopg  3897  xpid11  5000  sqxpeq0  5206  cores2  5295  funcoeqres  5665  dftpos2  6522  ine0  8711  fisumcom2  12183  fisum0diag2  12192  mertenslemi1  12280  fprodcom2fi  12371  fprodmodd  12386  bitsinv1  12707  4sqlem10  13144  ballotfilemgun  13246  setsslnid  13382  xpsff1o  13647  eqglact  14005  oppr1g  14361  dvmptccn  15739  dvmptc  15741  dvmptfsum  15749  fsumdvdsmul  16019  nninffeq  16968