Theorem 3eqtr2ri 2854

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

Syntax hints:   = wceq 1536

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817

This theorem is referenced by:  funimacnv  6438  uniqs  8360  ackbij1lem13  9657  ef01bndlem  15540  cos2bnd  15544  divalglem2  15749  decexp2  16414  lefld  17839  smndex2dlinvh  18085  discmp  22009  unmbl  24141  sinhalfpilem  25052  log2cnv  25525  lgam1  25644  ip0i  28605  polid2i  28937  hh0v  28948  pjinormii  29456  dfdec100  30550  dpmul100  30577  dpmul  30593  dpmul4  30594  subfacp1lem3  32433  uniqsALTV  35590  cotrclrcl  40093  sqwvfoura  42520  sqwvfourb  42521