Theorem 3eqtr4a 2288

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  uniintsnr  3962  fndmdifcom  5749  funopsn  5825  offres  6292  1stval2  6313  2ndval2  6314  ecovcom  6806  ecovass  6808  ecovdi  6810  nnnninfeq2  7319  zeo  9575  xnegneg  10058  xaddcom  10086  xaddid1  10087  xnegdi  10093  fzsuc2  10304  expnegap0  10799  facp1  10982  bcpasc  11018  hashfzp1  11078  resunimafz0  11085  ccat1st1st  11208  absexp  11630  iooinsup  11828  fsumf1o  11941  fsumadd  11957  fisumrev2  11997  fsumparts  12021  fprodf1o  12139  fprodmul  12142  efexp  12233  tanval2ap  12264  gcdcom  12534  gcd0id  12540  dfgcd3  12571  gcdass  12576  lcmcom  12626  lcmneg  12636  lcmass  12647  sqrt2irrlem  12723  nn0gcdsq  12762  dfphi2  12782  eulerthlemth  12794  pcneg  12888  setscom  13112  gsumfzfsumlem0  14590  restco  14888  txtopon  14976  dvmptid  15430  dvef  15441  fsumdvdsmul  15705  lgsneg  15743  lgsneg1  15744  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsquad2lem2  15801