Theorem 3eqtr2rd 2269

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  difinfsn  7290  nnnninfeq  7318  prarloclemlo  7704  recexgt0sr  7983  xp1d2m1eqxm1d2  9387  qnegmod  10621  modqeqmodmin  10646  faclbnd2  10994  cats1un  11292  cjmulval  11439  fsumsplit  11958  fzosump1  11968  isumclim3  11974  bcxmas  12040  trireciplem  12051  geo2sum  12065  geo2lim  12067  geoisum1c  12071  cvgratnnlemseq  12077  mertenslemi1  12086  fprodsplitdc  12147  eftlub  12241  addsin  12293  subsin  12294  subcos  12298  qredeu  12659  nn0sqrtelqelz  12768  4sqlem15  12968  strslfv2d  13115  mulgaddcomlem  13722  conjghm  13853  dvexp  15425  tangtx  15552  logsqrt  15637  mpodvdsmulf1o  15704  lgsquad2lem1  15800  2sqlem8  15842