Theorem 3eqtr2rd 2233

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  difinfsn  7159  nnnninfeq  7187  prarloclemlo  7554  recexgt0sr  7833  xp1d2m1eqxm1d2  9235  qnegmod  10440  modqeqmodmin  10465  faclbnd2  10813  cjmulval  11032  fsumsplit  11550  fzosump1  11560  isumclim3  11566  bcxmas  11632  trireciplem  11643  geo2sum  11657  geo2lim  11659  geoisum1c  11663  cvgratnnlemseq  11669  mertenslemi1  11678  fprodsplitdc  11739  eftlub  11833  addsin  11885  subsin  11886  subcos  11890  qredeu  12235  nn0sqrtelqelz  12344  4sqlem15  12543  strslfv2d  12661  mulgaddcomlem  13215  conjghm  13346  dvexp  14860  tangtx  14973  logsqrt  15057  2sqlem8  15210