Theorem 3eqtr2ri 2773

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 2769	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2767	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  funimacnv  6515  uniqs  8566  ackbij1lem13  9988  ef01bndlem  15893  cos2bnd  15897  divalglem2  16104  decexp2  16776  lefld  18310  smndex2dlinvh  18556  discmp  22549  unmbl  24701  sinhalfpilem  25620  log2cnv  26094  lgam1  26213  ip0i  29187  polid2i  29519  hh0v  29530  pjinormii  30038  dfdec100  31144  dpmul100  31171  dpmul  31187  dpmul4  31188  subfacp1lem3  33144  uniqsALTV  36464  cotrclrcl  41350  sqwvfoura  43769  sqwvfourb  43770