Theorem 3eqtr3g 2290

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

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

This theorem is referenced by:  csbnest1g  3197  disjdif2  3592  dfopg  3886  xpid11  4985  sqxpeq0  5191  cores2  5280  funcoeqres  5650  dftpos2  6505  ine0  8684  fisumcom2  12149  fisum0diag2  12158  mertenslemi1  12246  fprodcom2fi  12337  fprodmodd  12352  bitsinv1  12673  4sqlem10  13110  ballotfilemgun  13212  setsslnid  13348  xpsff1o  13613  eqglact  13978  oppr1g  14326  dvmptccn  15706  dvmptc  15708  dvmptfsum  15716  fsumdvdsmul  15985  nninffeq  16924