Theorem 3eqtr2ri 2769

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

Syntax hints:   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  funimacnv  6648  uniqs  8815  ackbij1lem13  10268  ef01bndlem  16216  cos2bnd  16220  divalglem2  16428  decexp2  17108  lefld  18649  smndex2dlinvh  18942  discmp  23421  unmbl  25585  sinhalfpilem  26519  log2cnv  27001  lgam1  27121  ip0i  30853  polid2i  31185  hh0v  31196  pjinormii  31704  dfdec100  32836  dpmul100  32863  dpmul  32879  dpmul4  32880  subfacp1lem3  35166  uniqsALTV  38310  redvmptabs  42368  cotrclrcl  43731  sqwvfoura  46183  sqwvfourb  46184