Theorem 3eqtr2rd 2278

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  difinfsn  7446  nnnninfeq  7474  prarloclemlo  7867  recexgt0sr  8146  xp1d2m1eqxm1d2  9569  qnegmod  10826  modqeqmodmin  10851  faclbnd2  11201  cats1un  11514  cjmulval  11674  sq01  11681  fsumsplit  12198  fzosump1  12208  isumclim3  12214  bcxmas  12280  trireciplem  12291  geo2sum  12305  geo2lim  12307  geoisum1c  12311  cvgratnnlemseq  12317  mertenslemi1  12326  fprodsplitdc  12387  eftlub  12481  addsin  12533  subsin  12534  subcos  12538  qredeu  12899  nn0sqrtelqelz  13010  4sqlem15  13212  strslfv2d  13452  mulgaddcomlem  14006  conjghm  14137  gsumresfi  14262  dvexp  15954  tangtx  16082  logsqrt  16175  mpodvdsmulf1o  16301  chtqub  16313  lgsquad2lem1  16422  2sqlem8  16464