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  3180  disjdif2  3570  dfopg  3855  xpid11  4947  sqxpeq0  5152  cores2  5241  funcoeqres  5605  dftpos2  6413  ine0  8551  fisumcom2  11965  fisum0diag2  11974  mertenslemi1  12062  fprodcom2fi  12153  fprodmodd  12168  bitsinv1  12489  4sqlem10  12926  setsslnid  13100  xpsff1o  13398  eqglact  13778  oppr1g  14061  dvmptccn  15405  dvmptc  15407  dvmptfsum  15415  fsumdvdsmul  15681  nninffeq  16474