Theorem 3eqtr4a 2297

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  uniintsnr  4006  fndmdifcom  5815  funopsn  5891  offres  6368  1stval2  6389  2ndval2  6390  ecovcom  6916  ecovass  6918  ecovdi  6920  nnnninfeq2  7470  zeo  9756  xnegneg  10246  xaddcom  10274  xaddid1  10275  xnegdi  10281  fzsuc2  10497  expnegap0  10999  resq01  11110  facp1  11184  bcpasc  11220  hashfzp1  11281  resunimafz0  11290  hashfibclem  11298  hashfibc  11299  hashf1  11303  ccat1st1st  11425  sq01  11676  absexp  11862  iooinsup  12062  fsumf1o  12176  fsumadd  12192  fisumrev2  12232  fsumparts  12256  fprodf1o  12374  fprodmul  12377  efexp  12468  tanval2ap  12499  gcdcom  12769  gcd0id  12775  dfgcd3  12806  gcdass  12811  lcmcom  12861  lcmneg  12871  lcmass  12882  sqrt2irrlem  12959  nn0gcdsq  12999  dfphi2  13021  eulerthlemth  13033  pcneg  13127  setscom  13444  restco  15366  txtopon  15454  dvmptid  15908  dvef  15919  logfac  16090  log2tlbndlog2  16181  fsumdvdsmul  16246  bcp1ctr  16267  lgsneg  16309  lgsneg1  16310  lgsdir2  16318  lgsdir  16320  lgsdi  16322  lgsquad2lem2  16367  egrsubgr  16670