Theorem 3eqtr2rd 2271

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  difinfsn  7299  nnnninfeq  7327  prarloclemlo  7714  recexgt0sr  7993  xp1d2m1eqxm1d2  9397  qnegmod  10632  modqeqmodmin  10657  faclbnd2  11005  cats1un  11306  cjmulval  11466  fsumsplit  11986  fzosump1  11996  isumclim3  12002  bcxmas  12068  trireciplem  12079  geo2sum  12093  geo2lim  12095  geoisum1c  12099  cvgratnnlemseq  12105  mertenslemi1  12114  fprodsplitdc  12175  eftlub  12269  addsin  12321  subsin  12322  subcos  12326  qredeu  12687  nn0sqrtelqelz  12796  4sqlem15  12996  strslfv2d  13143  mulgaddcomlem  13750  conjghm  13881  dvexp  15454  tangtx  15581  logsqrt  15666  mpodvdsmulf1o  15733  lgsquad2lem1  15829  2sqlem8  15871