Theorem 3eqtr4a 2229

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  uniintsnr  3867  fndmdifcom  5602  offres  6114  1stval2  6134  2ndval2  6135  ecovcom  6620  ecovass  6622  ecovdi  6624  nnnninfeq2  7105  zeo  9317  xnegneg  9790  xaddcom  9818  xaddid1  9819  xnegdi  9825  fzsuc2  10035  expnegap0  10484  facp1  10664  bcpasc  10700  hashfzp1  10759  resunimafz0  10766  absexp  11043  iooinsup  11240  fsumf1o  11353  fsumadd  11369  fisumrev2  11409  fsumparts  11433  fprodf1o  11551  fprodmul  11554  efexp  11645  tanval2ap  11676  gcdcom  11928  gcd0id  11934  dfgcd3  11965  gcdass  11970  lcmcom  12018  lcmneg  12028  lcmass  12039  sqrt2irrlem  12115  nn0gcdsq  12154  dfphi2  12174  eulerthlemth  12186  pcneg  12278  setscom  12456  restco  12968  txtopon  13056  dvef  13482  lgsneg  13719  lgsneg1  13720  lgsdir2  13728  lgsdir  13730  lgsdi  13732