Theorem 3eqtr2ri 2651

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

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  funimacnv  5970  uniqs  7807  ackbij1lem13  9054  ef01bndlem  14914  cos2bnd  14918  divalglem2  15118  decexp2  15779  lefld  17226  discmp  21201  unmbl  23305  sinhalfpilem  24215  log2cnv  24671  lgam1  24790  ip0i  27680  polid2i  28014  hh0v  28025  pjinormii  28535  dfdec100  29576  dpmul100  29605  dpmul  29621  dpmul4  29622  subfacp1lem3  31164  uniqsALTV  34101  cotrclrcl  38034  sqwvfoura  40445  sqwvfourb  40446