Theorem 3eqtr2ri 2764

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  funimacnv  6571  uniqs  8709  ackbij1lem13  10139  ef01bndlem  16107  cos2bnd  16111  divalglem2  16320  lefld  18513  smndex2dlinvh  18840  discmp  23340  unmbl  25492  sinhalfpilem  26426  log2cnv  26908  lgam1  27028  ip0i  30849  polid2i  31181  hh0v  31192  pjinormii  31700  dfdec100  32860  dpmul100  32927  dpmul  32943  dpmul4  32944  subfacp1lem3  35325  dmcnvep  38512  redvmptabs  42557  cotrclrcl  43925  sqwvfoura  46414  sqwvfourb  46415