Theorem 3eqtr2ri 2795

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  funimacnv  6621  uniqs  8777  ackbij1lem13  10230  ef01bndlem  16262  cos2bnd  16266  divalglem2  16475  lefld  18670  smndex2dlinvh  19016  discmp  23605  unmbl  25747  sinhalfpilem  26679  log2cnv  27160  lgam1  27279  ip0i  31248  polid2i  31580  hh0v  31591  pjinormii  32099  dfdec100  33244  dpmul100  33286  dpmul  33302  dpmul4  33303  subfacp1lem3  35711  dmcnvep  39095  25or6to4  43031  redvmptabs  43179  cotrclrcl  44526  sqwvfoura  47000  sqwvfourb  47001