Theorem 3eqtr4a 2255

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 2245	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2232	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  uniintsnr  3910  fndmdifcom  5668  offres  6192  1stval2  6213  2ndval2  6214  ecovcom  6701  ecovass  6703  ecovdi  6705  nnnninfeq2  7195  zeo  9431  xnegneg  9908  xaddcom  9936  xaddid1  9937  xnegdi  9943  fzsuc2  10154  expnegap0  10639  facp1  10822  bcpasc  10858  hashfzp1  10916  resunimafz0  10923  absexp  11244  iooinsup  11442  fsumf1o  11555  fsumadd  11571  fisumrev2  11611  fsumparts  11635  fprodf1o  11753  fprodmul  11756  efexp  11847  tanval2ap  11878  gcdcom  12140  gcd0id  12146  dfgcd3  12177  gcdass  12182  lcmcom  12232  lcmneg  12242  lcmass  12253  sqrt2irrlem  12329  nn0gcdsq  12368  dfphi2  12388  eulerthlemth  12400  pcneg  12494  setscom  12718  gsumfzfsumlem0  14142  restco  14410  txtopon  14498  dvmptid  14952  dvef  14963  fsumdvdsmul  15227  lgsneg  15265  lgsneg1  15266  lgsdir2  15274  lgsdir  15276  lgsdi  15278  lgsquad2lem2  15323