Theorem 3eqtr4a 2293

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  uniintsnr  3990  fndmdifcom  5789  funopsn  5865  offres  6341  1stval2  6362  2ndval2  6363  ecovcom  6889  ecovass  6891  ecovdi  6893  nnnninfeq2  7433  zeo  9701  xnegneg  10185  xaddcom  10213  xaddid1  10214  xnegdi  10220  fzsuc2  10435  expnegap0  10933  resq01  11044  facp1  11117  bcpasc  11153  hashfzp1  11214  resunimafz0  11223  hashfibclem  11231  hashfibc  11232  ccat1st1st  11354  absexp  11789  iooinsup  11987  fsumf1o  12101  fsumadd  12117  fisumrev2  12157  fsumparts  12181  fprodf1o  12299  fprodmul  12302  efexp  12393  tanval2ap  12424  gcdcom  12694  gcd0id  12700  dfgcd3  12731  gcdass  12736  lcmcom  12786  lcmneg  12796  lcmass  12807  sqrt2irrlem  12883  nn0gcdsq  12922  dfphi2  12942  eulerthlemth  12954  pcneg  13048  setscom  13336  gsumfzfsumlem0  14860  restco  15165  txtopon  15253  dvmptid  15707  dvef  15718  fsumdvdsmul  15985  lgsneg  16023  lgsneg1  16024  lgsdir2  16032  lgsdir  16034  lgsdi  16036  lgsquad2lem2  16081  egrsubgr  16384