Theorem 3eqtr4a 2289

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212

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

This theorem is referenced by:  uniintsnr  3963  fndmdifcom  5753  funopsn  5830  offres  6299  1stval2  6320  2ndval2  6321  ecovcom  6813  ecovass  6815  ecovdi  6817  nnnninfeq2  7330  zeo  9587  xnegneg  10070  xaddcom  10098  xaddid1  10099  xnegdi  10105  fzsuc2  10316  expnegap0  10812  facp1  10995  bcpasc  11031  hashfzp1  11091  resunimafz0  11098  ccat1st1st  11224  absexp  11659  iooinsup  11857  fsumf1o  11971  fsumadd  11987  fisumrev2  12027  fsumparts  12051  fprodf1o  12169  fprodmul  12172  efexp  12263  tanval2ap  12294  gcdcom  12564  gcd0id  12570  dfgcd3  12601  gcdass  12606  lcmcom  12656  lcmneg  12666  lcmass  12677  sqrt2irrlem  12753  nn0gcdsq  12792  dfphi2  12812  eulerthlemth  12824  pcneg  12918  setscom  13142  gsumfzfsumlem0  14621  restco  14924  txtopon  15012  dvmptid  15466  dvef  15477  fsumdvdsmul  15741  lgsneg  15779  lgsneg1  15780  lgsdir2  15788  lgsdir  15790  lgsdi  15792  lgsquad2lem2  15837  egrsubgr  16140