Theorem 3eqtr2ri 2759

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 2755	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2753	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  funimacnv  6581  uniqs  8724  ackbij1lem13  10160  ef01bndlem  16128  cos2bnd  16132  divalglem2  16341  lefld  18527  smndex2dlinvh  18820  discmp  23261  unmbl  25414  sinhalfpilem  26348  log2cnv  26830  lgam1  26950  ip0i  30727  polid2i  31059  hh0v  31070  pjinormii  31578  dfdec100  32728  dpmul100  32790  dpmul  32806  dpmul4  32807  subfacp1lem3  35142  dmcnvep  38334  redvmptabs  42321  cotrclrcl  43704  sqwvfoura  46199  sqwvfourb  46200