Theorem 3eqtr4a 2290

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  uniintsnr  3969  fndmdifcom  5762  funopsn  5838  offres  6306  1stval2  6327  2ndval2  6328  ecovcom  6854  ecovass  6856  ecovdi  6858  nnnninfeq2  7371  zeo  9629  xnegneg  10112  xaddcom  10140  xaddid1  10141  xnegdi  10147  fzsuc2  10359  expnegap0  10855  facp1  11038  bcpasc  11074  hashfzp1  11134  resunimafz0  11141  ccat1st1st  11267  absexp  11702  iooinsup  11900  fsumf1o  12014  fsumadd  12030  fisumrev2  12070  fsumparts  12094  fprodf1o  12212  fprodmul  12215  efexp  12306  tanval2ap  12337  gcdcom  12607  gcd0id  12613  dfgcd3  12644  gcdass  12649  lcmcom  12699  lcmneg  12709  lcmass  12720  sqrt2irrlem  12796  nn0gcdsq  12835  dfphi2  12855  eulerthlemth  12867  pcneg  12961  setscom  13185  gsumfzfsumlem0  14665  restco  14968  txtopon  15056  dvmptid  15510  dvef  15521  fsumdvdsmul  15788  lgsneg  15826  lgsneg1  15827  lgsdir2  15835  lgsdir  15837  lgsdi  15839  lgsquad2lem2  15884  egrsubgr  16187