Theorem 3eqtr4rd 2126

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
2		3eqtr4d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtr4d 2118	. 2 ⊢ (𝜑 → 𝐷 = 𝐴)
4		3eqtr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
5	3, 4	eqtr4d 2118	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076

This theorem is referenced by:  csbcnvg  4567  phplem4  6411  phplem4on  6423  recexnq  6694  prarloclemcalc  6806  addcomprg  6882  mulcomprg  6884  mulcmpblnrlemg  7031  axmulass  7153  divnegap  7913  modqlt  9467  modqmulnn  9476  iseqvalt  9584  iseqcaopr3  9608  ibcval5  9839  omgadd  9878  cjreb  9954  recj  9955  imcj  9963  imval2  9982  resqrexlemover  10097  sqrtmul  10122  amgm2  10205  maxabslemab  10293  flodddiv4  10541  dfgcd3  10606  absmulgcd  10613  sqpweven  10760  2sqpwodd  10761  crth  10807