Theorem 3eqtr4a 2252

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 2242	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2229	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  uniintsnr  3907  fndmdifcom  5665  offres  6189  1stval2  6210  2ndval2  6211  ecovcom  6698  ecovass  6700  ecovdi  6702  nnnninfeq2  7190  zeo  9425  xnegneg  9902  xaddcom  9930  xaddid1  9931  xnegdi  9937  fzsuc2  10148  expnegap0  10621  facp1  10804  bcpasc  10840  hashfzp1  10898  resunimafz0  10905  absexp  11226  iooinsup  11423  fsumf1o  11536  fsumadd  11552  fisumrev2  11592  fsumparts  11616  fprodf1o  11734  fprodmul  11737  efexp  11828  tanval2ap  11859  gcdcom  12113  gcd0id  12119  dfgcd3  12150  gcdass  12155  lcmcom  12205  lcmneg  12215  lcmass  12226  sqrt2irrlem  12302  nn0gcdsq  12341  dfphi2  12361  eulerthlemth  12373  pcneg  12466  setscom  12661  gsumfzfsumlem0  14085  restco  14353  txtopon  14441  dvmptid  14895  dvef  14906  lgsneg  15181  lgsneg1  15182  lgsdir2  15190  lgsdir  15192  lgsdi  15194  lgsquad2lem2  15239