Theorem 3eqtr2rd 2271

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  difinfsn  7342  nnnninfeq  7370  prarloclemlo  7757  recexgt0sr  8036  xp1d2m1eqxm1d2  9439  qnegmod  10677  modqeqmodmin  10702  faclbnd2  11050  cats1un  11351  cjmulval  11511  fsumsplit  12031  fzosump1  12041  isumclim3  12047  bcxmas  12113  trireciplem  12124  geo2sum  12138  geo2lim  12140  geoisum1c  12144  cvgratnnlemseq  12150  mertenslemi1  12159  fprodsplitdc  12220  eftlub  12314  addsin  12366  subsin  12367  subcos  12371  qredeu  12732  nn0sqrtelqelz  12841  4sqlem15  13041  strslfv2d  13188  mulgaddcomlem  13795  conjghm  13926  dvexp  15505  tangtx  15632  logsqrt  15717  mpodvdsmulf1o  15787  lgsquad2lem1  15883  2sqlem8  15925