Theorem 3eqtr2ri 2763

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

Syntax hints:   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720

This theorem is referenced by:  funimacnv  6639  uniqs  8802  ackbij1lem13  10263  ef01bndlem  16168  cos2bnd  16172  divalglem2  16379  decexp2  17051  lefld  18591  smndex2dlinvh  18876  discmp  23322  unmbl  25486  sinhalfpilem  26418  log2cnv  26896  lgam1  27016  ip0i  30655  polid2i  30987  hh0v  30998  pjinormii  31506  dfdec100  32614  dpmul100  32641  dpmul  32657  dpmul4  32658  subfacp1lem3  34825  uniqsALTV  37833  cotrclrcl  43203  sqwvfoura  45645  sqwvfourb  45646