Theorem 3eqtr2ri 2791

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 2787	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2785	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 2155  ax-ext 2733

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

This theorem is used by:  funimacnv  6622  uniqs  8795  ackbij1lem13  10310  ef01bndlem  16353  cos2bnd  16357  divalglem2  16566  lefld  18767  smndex2dlinvh  19117  discmp  23717  unmbl  25859  sinhalfpilem  26793  log2cnv  27273  lgam1  27392  ip0i  31428  polid2i  31760  hh0v  31771  pjinormii  32279  dfdec100  33422  dpmul100  33464  dpmul  33480  dpmul4  33481  subfacp1lem3  35948  dmcnvep  39322  25or6to4  43258  redvmptabs  43413  cotrclrcl  44743  sqwvfoura  47239  sqwvfourb  47240