Theorem 3eqtr4a 2263

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	⊢ 𝐴 = 𝐵
3eqtr4a.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4a.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtrdi 2253	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2240	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  uniintsnr  3920  fndmdifcom  5685  funopsn  5761  offres  6219  1stval2  6240  2ndval2  6241  ecovcom  6728  ecovass  6730  ecovdi  6732  nnnninfeq2  7230  zeo  9477  xnegneg  9954  xaddcom  9982  xaddid1  9983  xnegdi  9989  fzsuc2  10200  expnegap0  10690  facp1  10873  bcpasc  10909  hashfzp1  10967  resunimafz0  10974  absexp  11332  iooinsup  11530  fsumf1o  11643  fsumadd  11659  fisumrev2  11699  fsumparts  11723  fprodf1o  11841  fprodmul  11844  efexp  11935  tanval2ap  11966  gcdcom  12236  gcd0id  12242  dfgcd3  12273  gcdass  12278  lcmcom  12328  lcmneg  12338  lcmass  12349  sqrt2irrlem  12425  nn0gcdsq  12464  dfphi2  12484  eulerthlemth  12496  pcneg  12590  setscom  12814  gsumfzfsumlem0  14290  restco  14588  txtopon  14676  dvmptid  15130  dvef  15141  fsumdvdsmul  15405  lgsneg  15443  lgsneg1  15444  lgsdir2  15452  lgsdir  15454  lgsdi  15456  lgsquad2lem2  15501