Theorem 3eqtr4a 2225

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  uniintsnr  3860  fndmdifcom  5591  offres  6103  1stval2  6123  2ndval2  6124  ecovcom  6608  ecovass  6610  ecovdi  6612  nnnninfeq2  7093  zeo  9296  xnegneg  9769  xaddcom  9797  xaddid1  9798  xnegdi  9804  fzsuc2  10014  expnegap0  10463  facp1  10643  bcpasc  10679  hashfzp1  10737  resunimafz0  10744  absexp  11021  iooinsup  11218  fsumf1o  11331  fsumadd  11347  fisumrev2  11387  fsumparts  11411  fprodf1o  11529  fprodmul  11532  efexp  11623  tanval2ap  11654  gcdcom  11906  gcd0id  11912  dfgcd3  11943  gcdass  11948  lcmcom  11996  lcmneg  12006  lcmass  12017  sqrt2irrlem  12093  nn0gcdsq  12132  dfphi2  12152  eulerthlemth  12164  pcneg  12256  setscom  12434  restco  12814  txtopon  12902  dvef  13328  lgsneg  13565  lgsneg1  13566  lgsdir2  13574  lgsdir  13576  lgsdi  13578