Theorem 3eqtr2ri 2793

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  funimacnv  6617  uniqs  8767  ackbij1lem13  10210  ef01bndlem  16235  cos2bnd  16239  divalglem2  16448  lefld  18643  smndex2dlinvh  18974  discmp  23555  unmbl  25696  sinhalfpilem  26628  log2cnv  27109  lgam1  27228  ip0i  31177  polid2i  31509  hh0v  31520  pjinormii  32028  dfdec100  33174  dpmul100  33216  dpmul  33232  dpmul4  33233  subfacp1lem3  35674  dmcnvep  39037  25or6to4  42973  redvmptabs  43121  cotrclrcl  44468  sqwvfoura  46942  sqwvfourb  46943