Theorem 3eqtr4a 2288

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  uniintsnr  3959  fndmdifcom  5741  funopsn  5817  offres  6280  1stval2  6301  2ndval2  6302  ecovcom  6789  ecovass  6791  ecovdi  6793  nnnninfeq2  7296  zeo  9552  xnegneg  10029  xaddcom  10057  xaddid1  10058  xnegdi  10064  fzsuc2  10275  expnegap0  10769  facp1  10952  bcpasc  10988  hashfzp1  11046  resunimafz0  11053  ccat1st1st  11172  absexp  11590  iooinsup  11788  fsumf1o  11901  fsumadd  11917  fisumrev2  11957  fsumparts  11981  fprodf1o  12099  fprodmul  12102  efexp  12193  tanval2ap  12224  gcdcom  12494  gcd0id  12500  dfgcd3  12531  gcdass  12536  lcmcom  12586  lcmneg  12596  lcmass  12607  sqrt2irrlem  12683  nn0gcdsq  12722  dfphi2  12742  eulerthlemth  12754  pcneg  12848  setscom  13072  gsumfzfsumlem0  14550  restco  14848  txtopon  14936  dvmptid  15390  dvef  15401  fsumdvdsmul  15665  lgsneg  15703  lgsneg1  15704  lgsdir2  15712  lgsdir  15714  lgsdi  15716  lgsquad2lem2  15761