Theorem 3eqtr4a 2290

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

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

This theorem is referenced by:  uniintsnr  3969  fndmdifcom  5762  funopsn  5838  offres  6306  1stval2  6327  2ndval2  6328  ecovcom  6854  ecovass  6856  ecovdi  6858  nnnninfeq2  7388  zeo  9646  xnegneg  10129  xaddcom  10157  xaddid1  10158  xnegdi  10164  fzsuc2  10376  expnegap0  10872  facp1  11055  bcpasc  11091  hashfzp1  11151  resunimafz0  11158  ccat1st1st  11284  absexp  11719  iooinsup  11917  fsumf1o  12031  fsumadd  12047  fisumrev2  12087  fsumparts  12111  fprodf1o  12229  fprodmul  12232  efexp  12323  tanval2ap  12354  gcdcom  12624  gcd0id  12630  dfgcd3  12661  gcdass  12666  lcmcom  12716  lcmneg  12726  lcmass  12737  sqrt2irrlem  12813  nn0gcdsq  12852  dfphi2  12872  eulerthlemth  12884  pcneg  12978  setscom  13202  gsumfzfsumlem0  14682  restco  14985  txtopon  15073  dvmptid  15527  dvef  15538  fsumdvdsmul  15805  lgsneg  15843  lgsneg1  15844  lgsdir2  15852  lgsdir  15854  lgsdi  15856  lgsquad2lem2  15901  egrsubgr  16204