Theorem 3eqtr2rd 2210

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

Syntax hints:   → wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  difinfsn  7077  nnnninfeq  7104  prarloclemlo  7456  recexgt0sr  7735  xp1d2m1eqxm1d2  9130  qnegmod  10325  modqeqmodmin  10350  faclbnd2  10676  cjmulval  10852  fsumsplit  11370  fzosump1  11380  isumclim3  11386  bcxmas  11452  trireciplem  11463  geo2sum  11477  geo2lim  11479  geoisum1c  11483  cvgratnnlemseq  11489  mertenslemi1  11498  fprodsplitdc  11559  eftlub  11653  addsin  11705  subsin  11706  subcos  11710  qredeu  12051  nn0sqrtelqelz  12160  strslfv2d  12458  dvexp  13469  tangtx  13553  logsqrt  13637  2sqlem8  13753