Theorem 3eqtr3g 2285

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  csbnest1g  3181  disjdif2  3571  dfopg  3858  xpid11  4953  sqxpeq0  5158  cores2  5247  funcoeqres  5611  dftpos2  6422  ine0  8563  fisumcom2  11989  fisum0diag2  11998  mertenslemi1  12086  fprodcom2fi  12177  fprodmodd  12192  bitsinv1  12513  4sqlem10  12950  setsslnid  13124  xpsff1o  13422  eqglact  13802  oppr1g  14085  dvmptccn  15429  dvmptc  15431  dvmptfsum  15439  fsumdvdsmul  15705  nninffeq  16558