Theorem 3eqtr2ri 2759

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 2755	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2753	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 2701

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

This theorem is referenced by:  funimacnv  6597  uniqs  8747  ackbij1lem13  10184  ef01bndlem  16152  cos2bnd  16156  divalglem2  16365  lefld  18551  smndex2dlinvh  18844  discmp  23285  unmbl  25438  sinhalfpilem  26372  log2cnv  26854  lgam1  26974  ip0i  30754  polid2i  31086  hh0v  31097  pjinormii  31605  dfdec100  32755  dpmul100  32817  dpmul  32833  dpmul4  32834  subfacp1lem3  35169  dmcnvep  38361  redvmptabs  42348  cotrclrcl  43731  sqwvfoura  46226  sqwvfourb  46227