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  10827  modqeqmodmin  10852  faclbnd2  11202  cats1un  11515  cjmulval  11675  sq01  11682  fsumsplit  12199  fzosump1  12209  isumclim3  12215  bcxmas  12281  trireciplem  12292  geo2sum  12306  geo2lim  12308  geoisum1c  12312  cvgratnnlemseq  12318  mertenslemi1  12327  fprodsplitdc  12388  eftlub  12482  addsin  12534  subsin  12535  subcos  12539  qredeu  12900  nn0sqrtelqelz  13011  4sqlem15  13213  strslfv2d  13453  mulgaddcomlem  14007  conjghm  14138  gsumresfi  14263  dvexp  15937  tangtx  16065  logsqrt  16158  mpodvdsmulf1o  16284  chtqub  16296  lgsquad2lem1  16405  2sqlem8  16447