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  3911  fndmdifcom  5671  offres  6201  1stval2  6222  2ndval2  6223  ecovcom  6710  ecovass  6712  ecovdi  6714  nnnninfeq2  7204  zeo  9448  xnegneg  9925  xaddcom  9953  xaddid1  9954  xnegdi  9960  fzsuc2  10171  expnegap0  10656  facp1  10839  bcpasc  10875  hashfzp1  10933  resunimafz0  10940  absexp  11261  iooinsup  11459  fsumf1o  11572  fsumadd  11588  fisumrev2  11628  fsumparts  11652  fprodf1o  11770  fprodmul  11773  efexp  11864  tanval2ap  11895  gcdcom  12165  gcd0id  12171  dfgcd3  12202  gcdass  12207  lcmcom  12257  lcmneg  12267  lcmass  12278  sqrt2irrlem  12354  nn0gcdsq  12393  dfphi2  12413  eulerthlemth  12425  pcneg  12519  setscom  12743  gsumfzfsumlem0  14218  restco  14494  txtopon  14582  dvmptid  15036  dvef  15047  fsumdvdsmul  15311  lgsneg  15349  lgsneg1  15350  lgsdir2  15358  lgsdir  15360  lgsdi  15362  lgsquad2lem2  15407