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  7278  nnnninfeq  7306  prarloclemlo  7692  recexgt0sr  7971  xp1d2m1eqxm1d2  9375  qnegmod  10603  modqeqmodmin  10628  faclbnd2  10976  cats1un  11268  cjmulval  11414  fsumsplit  11933  fzosump1  11943  isumclim3  11949  bcxmas  12015  trireciplem  12026  geo2sum  12040  geo2lim  12042  geoisum1c  12046  cvgratnnlemseq  12052  mertenslemi1  12061  fprodsplitdc  12122  eftlub  12216  addsin  12268  subsin  12269  subcos  12273  qredeu  12634  nn0sqrtelqelz  12743  4sqlem15  12943  strslfv2d  13090  mulgaddcomlem  13697  conjghm  13828  dvexp  15400  tangtx  15527  logsqrt  15612  mpodvdsmulf1o  15679  lgsquad2lem1  15775  2sqlem8  15817