Theorem 3eqtr2ri 2761

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 2757	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2755	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 2121  ax-ext 2703

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

This theorem is referenced by:  funimacnv  6562  uniqs  8698  ackbij1lem13  10122  ef01bndlem  16093  cos2bnd  16097  divalglem2  16306  lefld  18498  smndex2dlinvh  18825  discmp  23313  unmbl  25465  sinhalfpilem  26399  log2cnv  26881  lgam1  27001  ip0i  30805  polid2i  31137  hh0v  31148  pjinormii  31656  dfdec100  32813  dpmul100  32877  dpmul  32893  dpmul4  32894  subfacp1lem3  35226  dmcnvep  38415  redvmptabs  42401  cotrclrcl  43783  sqwvfoura  46274  sqwvfourb  46275