Theorem 3eqtr4a 2264

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 |- ( ph -> C = A )
2		3eqtr4a.1	. . 3 |- A = B
3	1, 2	eqtrdi 2254	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2241	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  uniintsnr  3921  fndmdifcom  5686  funopsn  5762  offres  6220  1stval2  6241  2ndval2  6242  ecovcom  6729  ecovass  6731  ecovdi  6733  nnnninfeq2  7231  zeo  9478  xnegneg  9955  xaddcom  9983  xaddid1  9984  xnegdi  9990  fzsuc2  10201  expnegap0  10692  facp1  10875  bcpasc  10911  hashfzp1  10969  resunimafz0  10976  ccat1st1st  11093  absexp  11390  iooinsup  11588  fsumf1o  11701  fsumadd  11717  fisumrev2  11757  fsumparts  11781  fprodf1o  11899  fprodmul  11902  efexp  11993  tanval2ap  12024  gcdcom  12294  gcd0id  12300  dfgcd3  12331  gcdass  12336  lcmcom  12386  lcmneg  12396  lcmass  12407  sqrt2irrlem  12483  nn0gcdsq  12522  dfphi2  12542  eulerthlemth  12554  pcneg  12648  setscom  12872  gsumfzfsumlem0  14348  restco  14646  txtopon  14734  dvmptid  15188  dvef  15199  fsumdvdsmul  15463  lgsneg  15501  lgsneg1  15502  lgsdir2  15510  lgsdir  15512  lgsdi  15514  lgsquad2lem2  15559