Theorem 3eqtr2ri 2765

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  funimacnv  6617  uniqs  8791  ackbij1lem13  10245  ef01bndlem  16202  cos2bnd  16206  divalglem2  16414  lefld  18602  smndex2dlinvh  18895  discmp  23336  unmbl  25490  sinhalfpilem  26424  log2cnv  26906  lgam1  27026  ip0i  30806  polid2i  31138  hh0v  31149  pjinormii  31657  dfdec100  32809  dpmul100  32871  dpmul  32887  dpmul4  32888  subfacp1lem3  35204  uniqsALTV  38347  redvmptabs  42403  cotrclrcl  43766  sqwvfoura  46257  sqwvfourb  46258