Theorem 3eqtr2rd 2272

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 2268	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2266	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 2214

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

This theorem is referenced by:  difinfsn  7391  nnnninfeq  7419  prarloclemlo  7809  recexgt0sr  8088  xp1d2m1eqxm1d2  9491  qnegmod  10731  modqeqmodmin  10756  faclbnd2  11104  cats1un  11413  cjmulval  11573  fsumsplit  12093  fzosump1  12103  isumclim3  12109  bcxmas  12175  trireciplem  12186  geo2sum  12200  geo2lim  12202  geoisum1c  12206  cvgratnnlemseq  12212  mertenslemi1  12221  fprodsplitdc  12282  eftlub  12376  addsin  12428  subsin  12429  subcos  12433  qredeu  12794  nn0sqrtelqelz  12903  4sqlem15  13103  strslfv2d  13255  mulgaddcomlem  13862  conjghm  13993  dvexp  15576  tangtx  15703  logsqrt  15788  mpodvdsmulf1o  15858  lgsquad2lem1  15954  2sqlem8  15996