Theorem 3eqtr2ri 2828

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

Syntax hints:   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  funimacnv  6405  uniqs  8340  ackbij1lem13  9643  ef01bndlem  15529  cos2bnd  15533  divalglem2  15736  decexp2  16401  lefld  17828  smndex2dlinvh  18074  discmp  22003  unmbl  24141  sinhalfpilem  25056  log2cnv  25530  lgam1  25649  ip0i  28608  polid2i  28940  hh0v  28951  pjinormii  29459  dfdec100  30572  dpmul100  30599  dpmul  30615  dpmul4  30616  subfacp1lem3  32542  uniqsALTV  35746  cotrclrcl  40443  sqwvfoura  42870  sqwvfourb  42871