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 ⊢ (𝜑 → 𝐶 = 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  csbnest1g  3203  disjdif2  3606  dfopg  3902  xpid11  5005  sqxpeq0  5211  cores2  5300  funcoeqres  5670  dftpos2  6532  ine0  8723  fisumcom2  12224  fisum0diag2  12233  mertenslemi1  12321  fprodcom2fi  12412  fprodmodd  12427  bitsinv1  12748  4sqlem10  13189  ballotfilemgun  13320  setsslnid  13456  xpsff1o  13723  eqglact  14081  oppr1g  14472  dvmptccn  15907  dvmptc  15909  dvmptfsum  15917  chtdif  16225  ppidif  16230  fsumdvdsmul  16246  nninffeq  17229