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  7440  nnnninfeq  7468  prarloclemlo  7861  recexgt0sr  8140  xp1d2m1eqxm1d2  9558  qnegmod  10806  modqeqmodmin  10831  faclbnd2  11180  cats1un  11493  cjmulval  11653  sq01  11660  fsumsplit  12174  fzosump1  12184  isumclim3  12190  bcxmas  12256  trireciplem  12267  geo2sum  12281  geo2lim  12283  geoisum1c  12287  cvgratnnlemseq  12293  mertenslemi1  12302  fprodsplitdc  12363  eftlub  12457  addsin  12509  subsin  12510  subcos  12514  qredeu  12875  nn0sqrtelqelz  12984  4sqlem15  13184  strslfv2d  13395  mulgaddcomlem  13948  conjghm  14079  dvexp  15812  tangtx  15939  logsqrt  16025  mpodvdsmulf1o  16104  lgsquad2lem1  16200  2sqlem8  16242