Theorem 3eqtr4a 2252

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 2242	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2229	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  uniintsnr  3906  fndmdifcom  5664  offres  6187  1stval2  6208  2ndval2  6209  ecovcom  6696  ecovass  6698  ecovdi  6700  nnnninfeq2  7188  zeo  9422  xnegneg  9899  xaddcom  9927  xaddid1  9928  xnegdi  9934  fzsuc2  10145  expnegap0  10618  facp1  10801  bcpasc  10837  hashfzp1  10895  resunimafz0  10902  absexp  11223  iooinsup  11420  fsumf1o  11533  fsumadd  11549  fisumrev2  11589  fsumparts  11613  fprodf1o  11731  fprodmul  11734  efexp  11825  tanval2ap  11856  gcdcom  12110  gcd0id  12116  dfgcd3  12147  gcdass  12152  lcmcom  12202  lcmneg  12212  lcmass  12223  sqrt2irrlem  12299  nn0gcdsq  12338  dfphi2  12358  eulerthlemth  12370  pcneg  12463  setscom  12658  gsumfzfsumlem0  14074  restco  14342  txtopon  14430  dvef  14873  lgsneg  15140  lgsneg1  15141  lgsdir2  15149  lgsdir  15151  lgsdi  15153