Theorem 3eqtr2ri 2766

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

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

This theorem is referenced by:  funimacnv  6573  uniqs  8711  ackbij1lem13  10141  ef01bndlem  16109  cos2bnd  16113  divalglem2  16322  lefld  18515  smndex2dlinvh  18842  discmp  23342  unmbl  25494  sinhalfpilem  26428  log2cnv  26910  lgam1  27030  ip0i  30900  polid2i  31232  hh0v  31243  pjinormii  31751  dfdec100  32911  dpmul100  32978  dpmul  32994  dpmul4  32995  subfacp1lem3  35376  dmcnvep  38573  redvmptabs  42615  cotrclrcl  43983  sqwvfoura  46472  sqwvfourb  46473