Theorem 3eqtr3g 2226

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	|- ( ph -> A = B )
3eqtr3g.2	|- A = C
3eqtr3g.3	|- B = D

Assertion

Ref	Expression
3eqtr3g	|- ( ph -> C = D )

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 |- A = C
2		3eqtr3g.1	. . 3 |- ( ph -> A = B )
3	1, 2	eqtr3id 2217	. 2 |- ( ph -> C = B )
4		3eqtr3g.3	. 2 |- B = D
5	3, 4	eqtrdi 2219	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  csbnest1g  3104  disjdif2  3492  dfopg  3761  xpid11  4832  sqxpeq0  5032  cores2  5121  funcoeqres  5471  dftpos2  6237  ine0  8300  fisumcom2  11388  fisum0diag2  11397  mertenslemi1  11485  fprodcom2fi  11576  fprodmodd  11591  4sqlem10  12326  setsslnid  12454  dvmptccn  13432  nninffeq  14013