Theorem 3eqtr2ri 2765

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

Syntax hints:   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  funimacnv  6628  uniqs  8773  ackbij1lem13  10229  ef01bndlem  16131  cos2bnd  16135  divalglem2  16342  decexp2  17012  lefld  18549  smndex2dlinvh  18834  discmp  23122  unmbl  25286  sinhalfpilem  26209  log2cnv  26685  lgam1  26804  ip0i  30345  polid2i  30677  hh0v  30688  pjinormii  31196  dfdec100  32303  dpmul100  32330  dpmul  32346  dpmul4  32347  subfacp1lem3  34471  uniqsALTV  37501  cotrclrcl  42795  sqwvfoura  45242  sqwvfourb  45243