Theorem 3eqtr3g 2261

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

Syntax hints:   → wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  csbnest1g  3149  disjdif2  3539  dfopg  3817  xpid11  4901  sqxpeq0  5106  cores2  5195  funcoeqres  5553  dftpos2  6347  ine0  8466  fisumcom2  11749  fisum0diag2  11758  mertenslemi1  11846  fprodcom2fi  11937  fprodmodd  11952  bitsinv1  12273  4sqlem10  12710  setsslnid  12884  xpsff1o  13181  eqglact  13561  oppr1g  13844  dvmptccn  15187  dvmptc  15189  dvmptfsum  15197  fsumdvdsmul  15463  nninffeq  15957