Theorem 3eqtr2ri 2793

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 2789	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2787	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  funimacnv  6651  uniqs  8832  ackbij1lem13  10348  ef01bndlem  16396  cos2bnd  16400  divalglem2  16609  lefld  18816  smndex2dlinvh  19166  discmp  23771  unmbl  25913  sinhalfpilem  26849  log2cnv  27329  lgam1  27448  ip0i  31484  polid2i  31816  hh0v  31827  pjinormii  32335  dfdec100  33517  dpmul100  33559  dpmul  33575  dpmul4  33576  subfacp1lem3  36155  dmcnvep  39586  25or6to4  43522  redvmptabs  43677  cotrclrcl  45003  sqwvfoura  47511  sqwvfourb  47512