Theorem 3eqtr2ri 2775

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  funimacnv  6659  uniqs  8835  ackbij1lem13  10300  ef01bndlem  16232  cos2bnd  16236  divalglem2  16443  decexp2  17122  lefld  18662  smndex2dlinvh  18952  discmp  23427  unmbl  25591  sinhalfpilem  26523  log2cnv  27005  lgam1  27125  ip0i  30857  polid2i  31189  hh0v  31200  pjinormii  31708  dfdec100  32834  dpmul100  32861  dpmul  32877  dpmul4  32878  subfacp1lem3  35150  uniqsALTV  38285  cotrclrcl  43704  sqwvfoura  46149  sqwvfourb  46150