Theorem 3eqtr4a 2291

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 2281	. 2 |- ( ph -> C = B )
4		3eqtr4a.3	. 2 |- ( ph -> D = B )
5	3, 4	eqtr4d 2268	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 2214

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

This theorem is referenced by:  uniintsnr  3985  fndmdifcom  5784  funopsn  5860  offres  6328  1stval2  6349  2ndval2  6350  ecovcom  6876  ecovass  6878  ecovdi  6880  nnnninfeq2  7420  zeo  9683  xnegneg  10166  xaddcom  10194  xaddid1  10195  xnegdi  10201  fzsuc2  10413  expnegap0  10909  facp1  11092  bcpasc  11128  hashfzp1  11189  resunimafz0  11198  hashfibclem  11206  hashfibc  11207  ccat1st1st  11329  absexp  11764  iooinsup  11962  fsumf1o  12076  fsumadd  12092  fisumrev2  12132  fsumparts  12156  fprodf1o  12274  fprodmul  12277  efexp  12368  tanval2ap  12399  gcdcom  12669  gcd0id  12675  dfgcd3  12706  gcdass  12711  lcmcom  12761  lcmneg  12771  lcmass  12782  sqrt2irrlem  12858  nn0gcdsq  12897  dfphi2  12917  eulerthlemth  12929  pcneg  13023  setscom  13252  gsumfzfsumlem0  14734  restco  15039  txtopon  15127  dvmptid  15581  dvef  15592  fsumdvdsmul  15859  lgsneg  15897  lgsneg1  15898  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsquad2lem2  15955  egrsubgr  16258