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  11141  fsumsplit  11660  fzosump1  11670  isumclim3  11676  bcxmas  11742  trireciplem  11753  geo2sum  11767  geo2lim  11769  geoisum1c  11773  cvgratnnlemseq  11779  mertenslemi1  11788  fprodsplitdc  11849  eftlub  11943  addsin  11995  subsin  11996  subcos  12000  qredeu  12361  nn0sqrtelqelz  12470  4sqlem15  12670  strslfv2d  12817  mulgaddcomlem  13423  conjghm  13554  dvexp  15125  tangtx  15252  logsqrt  15337  mpodvdsmulf1o  15404  lgsquad2lem1  15500  2sqlem8  15542