Theorem 3eqtr2ri 2767

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  funimacnv  6581  uniqs  8722  ackbij1lem13  10153  ef01bndlem  16121  cos2bnd  16125  divalglem2  16334  lefld  18527  smndex2dlinvh  18854  discmp  23354  unmbl  25506  sinhalfpilem  26440  log2cnv  26922  lgam1  27042  ip0i  30913  polid2i  31245  hh0v  31256  pjinormii  31764  dfdec100  32922  dpmul100  32989  dpmul  33005  dpmul4  33006  subfacp1lem3  35398  dmcnvep  38639  redvmptabs  42730  cotrclrcl  44098  sqwvfoura  46586  sqwvfourb  46587