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  6563  uniqs  8701  ackbij1lem13  10125  ef01bndlem  16093  cos2bnd  16097  divalglem2  16306  lefld  18498  smndex2dlinvh  18791  discmp  23283  unmbl  25436  sinhalfpilem  26370  log2cnv  26852  lgam1  26972  ip0i  30769  polid2i  31101  hh0v  31112  pjinormii  31620  dfdec100  32775  dpmul100  32837  dpmul  32853  dpmul4  32854  subfacp1lem3  35155  dmcnvep  38347  redvmptabs  42333  cotrclrcl  43715  sqwvfoura  46209  sqwvfourb  46210