Theorem 3eqtr2ri 2639

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  funimacnv  5884  uniqs  7694  ackbij1lem13  8937  ef01bndlem  14753  cos2bnd  14757  divalglem2  14956  decexp2  15617  lefld  17049  discmp  21011  unmbl  23112  sinhalfpilem  24019  log2cnv  24471  lgam1  24590  ip0i  27064  polid2i  27398  hh0v  27409  pjinormii  27919  subfacp1lem3  30418  cotrclrcl  37053  sqwvfoura  39121  sqwvfourb  39122