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  7298  nnnninfeq  7326  prarloclemlo  7713  recexgt0sr  7992  xp1d2m1eqxm1d2  9396  qnegmod  10630  modqeqmodmin  10655  faclbnd2  11003  cats1un  11301  cjmulval  11448  fsumsplit  11967  fzosump1  11977  isumclim3  11983  bcxmas  12049  trireciplem  12060  geo2sum  12074  geo2lim  12076  geoisum1c  12080  cvgratnnlemseq  12086  mertenslemi1  12095  fprodsplitdc  12156  eftlub  12250  addsin  12302  subsin  12303  subcos  12307  qredeu  12668  nn0sqrtelqelz  12777  4sqlem15  12977  strslfv2d  13124  mulgaddcomlem  13731  conjghm  13862  dvexp  15434  tangtx  15561  logsqrt  15646  mpodvdsmulf1o  15713  lgsquad2lem1  15809  2sqlem8  15851