Theorem 3eqtr2rd 2177

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

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  difinfsn  6978  prarloclemlo  7295  recexgt0sr  7574  xp1d2m1eqxm1d2  8965  qnegmod  10135  modqeqmodmin  10160  faclbnd2  10481  cjmulval  10653  fsumsplit  11169  fzosump1  11179  isumclim3  11185  bcxmas  11251  trireciplem  11262  geo2sum  11276  geo2lim  11278  geoisum1c  11282  cvgratnnlemseq  11288  mertenslemi1  11297  eftlub  11385  addsin  11438  subsin  11439  subcos  11443  qredeu  11767  nn0sqrtelqelz  11873  strslfv2d  11990  dvexp  12833  tangtx  12908  nninfalllemn  13191