Theorem 3eqtr4a 2223

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

Syntax hints:   → wi 4   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  uniintsnr  3854  fndmdifcom  5585  offres  6095  1stval2  6115  2ndval2  6116  ecovcom  6599  ecovass  6601  ecovdi  6603  nnnninfeq2  7084  zeo  9287  xnegneg  9760  xaddcom  9788  xaddid1  9789  xnegdi  9795  fzsuc2  10004  expnegap0  10453  facp1  10632  bcpasc  10668  hashfzp1  10726  resunimafz0  10730  absexp  11007  iooinsup  11204  fsumf1o  11317  fsumadd  11333  fisumrev2  11373  fsumparts  11397  fprodf1o  11515  fprodmul  11518  efexp  11609  tanval2ap  11640  gcdcom  11891  gcd0id  11897  dfgcd3  11928  gcdass  11933  lcmcom  11975  lcmneg  11985  lcmass  11996  sqrt2irrlem  12070  nn0gcdsq  12109  dfphi2  12129  eulerthlemth  12141  pcneg  12233  setscom  12371  restco  12715  txtopon  12803  dvef  13229