Theorem 3eqtr4a 2255

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 2245	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2232	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  uniintsnr  3911  fndmdifcom  5669  offres  6193  1stval2  6214  2ndval2  6215  ecovcom  6702  ecovass  6704  ecovdi  6706  nnnninfeq2  7196  zeo  9433  xnegneg  9910  xaddcom  9938  xaddid1  9939  xnegdi  9945  fzsuc2  10156  expnegap0  10641  facp1  10824  bcpasc  10860  hashfzp1  10918  resunimafz0  10925  absexp  11246  iooinsup  11444  fsumf1o  11557  fsumadd  11573  fisumrev2  11613  fsumparts  11637  fprodf1o  11755  fprodmul  11758  efexp  11849  tanval2ap  11880  gcdcom  12150  gcd0id  12156  dfgcd3  12187  gcdass  12192  lcmcom  12242  lcmneg  12252  lcmass  12263  sqrt2irrlem  12339  nn0gcdsq  12378  dfphi2  12398  eulerthlemth  12410  pcneg  12504  setscom  12728  gsumfzfsumlem0  14152  restco  14420  txtopon  14508  dvmptid  14962  dvef  14973  fsumdvdsmul  15237  lgsneg  15275  lgsneg1  15276  lgsdir2  15284  lgsdir  15286  lgsdi  15288  lgsquad2lem2  15333