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  9450  xnegneg  9927  xaddcom  9955  xaddid1  9956  xnegdi  9962  fzsuc2  10173  expnegap0  10658  facp1  10841  bcpasc  10877  hashfzp1  10935  resunimafz0  10942  absexp  11263  iooinsup  11461  fsumf1o  11574  fsumadd  11590  fisumrev2  11630  fsumparts  11654  fprodf1o  11772  fprodmul  11775  efexp  11866  tanval2ap  11897  gcdcom  12167  gcd0id  12173  dfgcd3  12204  gcdass  12209  lcmcom  12259  lcmneg  12269  lcmass  12280  sqrt2irrlem  12356  nn0gcdsq  12395  dfphi2  12415  eulerthlemth  12427  pcneg  12521  setscom  12745  gsumfzfsumlem0  14220  restco  14518  txtopon  14606  dvmptid  15060  dvef  15071  fsumdvdsmul  15335  lgsneg  15373  lgsneg1  15374  lgsdir2  15382  lgsdir  15384  lgsdi  15386  lgsquad2lem2  15431