Theorem 3eqtr2ri 2792

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  funimacnv  6602  uniqs  8755  ackbij1lem13  10187  ef01bndlem  16216  cos2bnd  16220  divalglem2  16429  lefld  18624  smndex2dlinvh  18954  discmp  23458  unmbl  25599  sinhalfpilem  26528  log2cnv  27009  lgam1  27128  ip0i  31028  polid2i  31360  hh0v  31371  pjinormii  31879  dfdec100  33032  dpmul100  33074  dpmul  33090  dpmul4  33091  subfacp1lem3  35532  dmcnvep  38887  redvmptabs  42969  cotrclrcl  44318  sqwvfoura  46802  sqwvfourb  46803