Theorem 3eqtr2ri 2680

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

Syntax hints:   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  funimacnv  6008  uniqs  7850  ackbij1lem13  9092  ef01bndlem  14958  cos2bnd  14962  divalglem2  15165  decexp2  15826  lefld  17273  discmp  21249  unmbl  23351  sinhalfpilem  24260  log2cnv  24716  lgam1  24835  ip0i  27808  polid2i  28142  hh0v  28153  pjinormii  28663  dfdec100  29704  dpmul100  29733  dpmul  29749  dpmul4  29750  subfacp1lem3  31290  uniqsALTV  34242  cotrclrcl  38351  sqwvfoura  40763  sqwvfourb  40764