Theorem 3eqtr2rd 2180

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

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  difinfsn  6993  prarloclemlo  7326  recexgt0sr  7605  xp1d2m1eqxm1d2  8996  qnegmod  10173  modqeqmodmin  10198  faclbnd2  10520  cjmulval  10692  fsumsplit  11208  fzosump1  11218  isumclim3  11224  bcxmas  11290  trireciplem  11301  geo2sum  11315  geo2lim  11317  geoisum1c  11321  cvgratnnlemseq  11327  mertenslemi1  11336  eftlub  11433  addsin  11485  subsin  11486  subcos  11490  qredeu  11814  nn0sqrtelqelz  11920  strslfv2d  12040  dvexp  12883  tangtx  12967  logsqrt  13051  nninfalllemn  13377