Theorem 3eqtr2ri 2766

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

Syntax hints:   = wceq 1541

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  funimacnv  6587  uniqs  8723  ackbij1lem13  10177  ef01bndlem  16077  cos2bnd  16081  divalglem2  16288  decexp2  16958  lefld  18495  smndex2dlinvh  18741  discmp  22786  unmbl  24938  sinhalfpilem  25857  log2cnv  26331  lgam1  26450  ip0i  29830  polid2i  30162  hh0v  30173  pjinormii  30681  dfdec100  31796  dpmul100  31823  dpmul  31839  dpmul4  31840  subfacp1lem3  33863  uniqsALTV  36863  cotrclrcl  42136  sqwvfoura  44589  sqwvfourb  44590