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  7263  nnnninfeq  7291  prarloclemlo  7677  recexgt0sr  7956  xp1d2m1eqxm1d2  9360  qnegmod  10586  modqeqmodmin  10611  faclbnd2  10959  cats1un  11248  cjmulval  11394  fsumsplit  11913  fzosump1  11923  isumclim3  11929  bcxmas  11995  trireciplem  12006  geo2sum  12020  geo2lim  12022  geoisum1c  12026  cvgratnnlemseq  12032  mertenslemi1  12041  fprodsplitdc  12102  eftlub  12196  addsin  12248  subsin  12249  subcos  12253  qredeu  12614  nn0sqrtelqelz  12723  4sqlem15  12923  strslfv2d  13070  mulgaddcomlem  13677  conjghm  13808  dvexp  15379  tangtx  15506  logsqrt  15591  mpodvdsmulf1o  15658  lgsquad2lem1  15754  2sqlem8  15796