Theorem 3eqtr4a 2266

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  uniintsnr  3935  fndmdifcom  5709  funopsn  5785  offres  6243  1stval2  6264  2ndval2  6265  ecovcom  6752  ecovass  6754  ecovdi  6756  nnnninfeq2  7257  zeo  9513  xnegneg  9990  xaddcom  10018  xaddid1  10019  xnegdi  10025  fzsuc2  10236  expnegap0  10729  facp1  10912  bcpasc  10948  hashfzp1  11006  resunimafz0  11013  ccat1st1st  11131  absexp  11505  iooinsup  11703  fsumf1o  11816  fsumadd  11832  fisumrev2  11872  fsumparts  11896  fprodf1o  12014  fprodmul  12017  efexp  12108  tanval2ap  12139  gcdcom  12409  gcd0id  12415  dfgcd3  12446  gcdass  12451  lcmcom  12501  lcmneg  12511  lcmass  12522  sqrt2irrlem  12598  nn0gcdsq  12637  dfphi2  12657  eulerthlemth  12669  pcneg  12763  setscom  12987  gsumfzfsumlem0  14463  restco  14761  txtopon  14849  dvmptid  15303  dvef  15314  fsumdvdsmul  15578  lgsneg  15616  lgsneg1  15617  lgsdir2  15625  lgsdir  15627  lgsdi  15629  lgsquad2lem2  15674