Theorem 3eqtr2rd 2205

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  difinfsn  7065  nnnninfeq  7092  prarloclemlo  7435  recexgt0sr  7714  xp1d2m1eqxm1d2  9109  qnegmod  10304  modqeqmodmin  10329  faclbnd2  10655  cjmulval  10830  fsumsplit  11348  fzosump1  11358  isumclim3  11364  bcxmas  11430  trireciplem  11441  geo2sum  11455  geo2lim  11457  geoisum1c  11461  cvgratnnlemseq  11467  mertenslemi1  11476  fprodsplitdc  11537  eftlub  11631  addsin  11683  subsin  11684  subcos  11688  qredeu  12029  nn0sqrtelqelz  12138  strslfv2d  12436  dvexp  13325  tangtx  13409  logsqrt  13493  2sqlem8  13609