Theorem 3eqtr2rd 2244

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  difinfsn  7201  nnnninfeq  7229  prarloclemlo  7606  recexgt0sr  7885  xp1d2m1eqxm1d2  9289  qnegmod  10512  modqeqmodmin  10537  faclbnd2  10885  cjmulval  11170  fsumsplit  11689  fzosump1  11699  isumclim3  11705  bcxmas  11771  trireciplem  11782  geo2sum  11796  geo2lim  11798  geoisum1c  11802  cvgratnnlemseq  11808  mertenslemi1  11817  fprodsplitdc  11878  eftlub  11972  addsin  12024  subsin  12025  subcos  12029  qredeu  12390  nn0sqrtelqelz  12499  4sqlem15  12699  strslfv2d  12846  mulgaddcomlem  13452  conjghm  13583  dvexp  15154  tangtx  15281  logsqrt  15366  mpodvdsmulf1o  15433  lgsquad2lem1  15529  2sqlem8  15571