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  ccat1st1st  11091  absexp  11361  iooinsup  11559  fsumf1o  11672  fsumadd  11688  fisumrev2  11728  fsumparts  11752  fprodf1o  11870  fprodmul  11873  efexp  11964  tanval2ap  11995  gcdcom  12265  gcd0id  12271  dfgcd3  12302  gcdass  12307  lcmcom  12357  lcmneg  12367  lcmass  12378  sqrt2irrlem  12454  nn0gcdsq  12493  dfphi2  12513  eulerthlemth  12525  pcneg  12619  setscom  12843  gsumfzfsumlem0  14319  restco  14617  txtopon  14705  dvmptid  15159  dvef  15170  fsumdvdsmul  15434  lgsneg  15472  lgsneg1  15473  lgsdir2  15481  lgsdir  15483  lgsdi  15485  lgsquad2lem2  15530