Theorem 3eqtr4a 2236

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  uniintsnr  3882  fndmdifcom  5624  offres  6138  1stval2  6158  2ndval2  6159  ecovcom  6644  ecovass  6646  ecovdi  6648  nnnninfeq2  7129  zeo  9360  xnegneg  9835  xaddcom  9863  xaddid1  9864  xnegdi  9870  fzsuc2  10081  expnegap0  10530  facp1  10712  bcpasc  10748  hashfzp1  10806  resunimafz0  10813  absexp  11090  iooinsup  11287  fsumf1o  11400  fsumadd  11416  fisumrev2  11456  fsumparts  11480  fprodf1o  11598  fprodmul  11601  efexp  11692  tanval2ap  11723  gcdcom  11976  gcd0id  11982  dfgcd3  12013  gcdass  12018  lcmcom  12066  lcmneg  12076  lcmass  12087  sqrt2irrlem  12163  nn0gcdsq  12202  dfphi2  12222  eulerthlemth  12234  pcneg  12326  setscom  12504  restco  13713  txtopon  13801  dvef  14227  lgsneg  14464  lgsneg1  14465  lgsdir2  14473  lgsdir  14475  lgsdi  14477