Theorem 3eqtr2ri 2760

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  funimacnv  6600  uniqs  8750  ackbij1lem13  10191  ef01bndlem  16159  cos2bnd  16163  divalglem2  16372  lefld  18558  smndex2dlinvh  18851  discmp  23292  unmbl  25445  sinhalfpilem  26379  log2cnv  26861  lgam1  26981  ip0i  30761  polid2i  31093  hh0v  31104  pjinormii  31612  dfdec100  32762  dpmul100  32824  dpmul  32840  dpmul4  32841  subfacp1lem3  35176  dmcnvep  38368  redvmptabs  42355  cotrclrcl  43738  sqwvfoura  46233  sqwvfourb  46234