Theorem 3eqtr2ri 2853

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2ri	⊢ 𝐷 = 𝐴

Proof of Theorem 3eqtr2ri

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2849	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2847	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  funimacnv  6437  uniqs  8359  ackbij1lem13  9656  ef01bndlem  15539  cos2bnd  15543  divalglem2  15748  decexp2  16413  lefld  17838  smndex2dlinvh  18084  discmp  22008  unmbl  24140  sinhalfpilem  25051  log2cnv  25524  lgam1  25643  ip0i  28604  polid2i  28936  hh0v  28947  pjinormii  29455  dfdec100  30548  dpmul100  30575  dpmul  30591  dpmul4  30592  subfacp1lem3  32431  uniqsALTV  35588  cotrclrcl  40094  sqwvfoura  42520  sqwvfourb  42521