Theorem 3eqtr4a 2263

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  uniintsnr  3920  fndmdifcom  5680  offres  6210  1stval2  6231  2ndval2  6232  ecovcom  6719  ecovass  6721  ecovdi  6723  nnnninfeq2  7213  zeo  9460  xnegneg  9937  xaddcom  9965  xaddid1  9966  xnegdi  9972  fzsuc2  10183  expnegap0  10673  facp1  10856  bcpasc  10892  hashfzp1  10950  resunimafz0  10957  absexp  11309  iooinsup  11507  fsumf1o  11620  fsumadd  11636  fisumrev2  11676  fsumparts  11700  fprodf1o  11818  fprodmul  11821  efexp  11912  tanval2ap  11943  gcdcom  12213  gcd0id  12219  dfgcd3  12250  gcdass  12255  lcmcom  12305  lcmneg  12315  lcmass  12326  sqrt2irrlem  12402  nn0gcdsq  12441  dfphi2  12461  eulerthlemth  12473  pcneg  12567  setscom  12791  gsumfzfsumlem0  14266  restco  14564  txtopon  14652  dvmptid  15106  dvef  15117  fsumdvdsmul  15381  lgsneg  15419  lgsneg1  15420  lgsdir2  15428  lgsdir  15430  lgsdi  15432  lgsquad2lem2  15477