Theorem 3eqtr2rd 2278

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  difinfsn  7441  nnnninfeq  7469  prarloclemlo  7862  recexgt0sr  8141  xp1d2m1eqxm1d2  9563  qnegmod  10821  modqeqmodmin  10846  faclbnd2  11196  cats1un  11509  cjmulval  11669  sq01  11676  fsumsplit  12193  fzosump1  12203  isumclim3  12209  bcxmas  12275  trireciplem  12286  geo2sum  12300  geo2lim  12302  geoisum1c  12306  cvgratnnlemseq  12312  mertenslemi1  12321  fprodsplitdc  12382  eftlub  12476  addsin  12528  subsin  12529  subcos  12533  qredeu  12894  nn0sqrtelqelz  13005  4sqlem15  13207  strslfv2d  13447  mulgaddcomlem  14001  conjghm  14132  dvexp  15903  tangtx  16031  logsqrt  16120  mpodvdsmulf1o  16245  chtqub  16257  lgsquad2lem1  16366  2sqlem8  16408