Theorem 3eqtr2ri 2790

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  funimacnv  6626  uniqs  8801  ackbij1lem13  10316  ef01bndlem  16361  cos2bnd  16365  divalglem2  16574  lefld  18775  smndex2dlinvh  19125  discmp  23725  unmbl  25867  sinhalfpilem  26801  log2cnv  27281  lgam1  27400  ip0i  31436  polid2i  31768  hh0v  31779  pjinormii  32287  dfdec100  33471  dpmul100  33513  dpmul  33529  dpmul4  33530  subfacp1lem3  36037  dmcnvep  39429  25or6to4  43365  redvmptabs  43520  cotrclrcl  44851  sqwvfoura  47346  sqwvfourb  47347