Theorem 3eqtr3g 2263

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 2254	. 2 |- ( ph -> C = B )
4		3eqtr3g.3	. 2 |- B = D
5	3, 4	eqtrdi 2256	1 |- ( ph -> C = D )

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  csbnest1g  3157  disjdif2  3547  dfopg  3831  xpid11  4920  sqxpeq0  5125  cores2  5214  funcoeqres  5575  dftpos2  6370  ine0  8501  fisumcom2  11864  fisum0diag2  11873  mertenslemi1  11961  fprodcom2fi  12052  fprodmodd  12067  bitsinv1  12388  4sqlem10  12825  setsslnid  12999  xpsff1o  13296  eqglact  13676  oppr1g  13959  dvmptccn  15302  dvmptc  15304  dvmptfsum  15312  fsumdvdsmul  15578  nninffeq  16159