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  6568  uniqs  8704  ackbij1lem13  10128  ef01bndlem  16099  cos2bnd  16103  divalglem2  16312  lefld  18504  smndex2dlinvh  18831  discmp  23319  unmbl  25471  sinhalfpilem  26405  log2cnv  26887  lgam1  27007  ip0i  30812  polid2i  31144  hh0v  31155  pjinormii  31663  dfdec100  32820  dpmul100  32884  dpmul  32900  dpmul4  32901  subfacp1lem3  35233  dmcnvep  38418  redvmptabs  42459  cotrclrcl  43840  sqwvfoura  46331  sqwvfourb  46332