Theorem 3eqtr2rd 2229

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

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

This theorem is referenced by:  difinfsn  7128  nnnninfeq  7155  prarloclemlo  7522  recexgt0sr  7801  xp1d2m1eqxm1d2  9200  qnegmod  10399  modqeqmodmin  10424  faclbnd2  10753  cjmulval  10928  fsumsplit  11446  fzosump1  11456  isumclim3  11462  bcxmas  11528  trireciplem  11539  geo2sum  11553  geo2lim  11555  geoisum1c  11559  cvgratnnlemseq  11565  mertenslemi1  11574  fprodsplitdc  11635  eftlub  11729  addsin  11781  subsin  11782  subcos  11786  qredeu  12128  nn0sqrtelqelz  12237  4sqlem15  12436  strslfv2d  12554  mulgaddcomlem  13082  conjghm  13212  dvexp  14627  tangtx  14711  logsqrt  14795  2sqlem8  14923