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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  funimacnv  6499  uniqs  8524  ackbij1lem13  9919  ef01bndlem  15821  cos2bnd  15825  divalglem2  16032  decexp2  16704  lefld  18225  smndex2dlinvh  18471  discmp  22457  unmbl  24606  sinhalfpilem  25525  log2cnv  25999  lgam1  26118  ip0i  29088  polid2i  29420  hh0v  29431  pjinormii  29939  dfdec100  31046  dpmul100  31073  dpmul  31089  dpmul4  31090  subfacp1lem3  33044  uniqsALTV  36391  cotrclrcl  41239  sqwvfoura  43659  sqwvfourb  43660