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  6619  uniqs  8787  ackbij1lem13  10302  ef01bndlem  16345  cos2bnd  16349  divalglem2  16558  lefld  18759  smndex2dlinvh  19109  discmp  23709  unmbl  25851  sinhalfpilem  26785  log2cnv  27265  lgam1  27384  ip0i  31420  polid2i  31752  hh0v  31763  pjinormii  32271  dfdec100  33414  dpmul100  33456  dpmul  33472  dpmul4  33473  subfacp1lem3  35926  dmcnvep  39300  25or6to4  43236  redvmptabs  43391  cotrclrcl  44727  sqwvfoura  47207  sqwvfourb  47208