Theorem 3eqtr2ri 2766

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  funimacnv  6579  uniqs  8720  ackbij1lem13  10153  ef01bndlem  16151  cos2bnd  16155  divalglem2  16364  lefld  18558  smndex2dlinvh  18888  discmp  23363  unmbl  25504  sinhalfpilem  26427  log2cnv  26908  lgam1  27027  ip0i  30896  polid2i  31228  hh0v  31239  pjinormii  31747  dfdec100  32903  dpmul100  32956  dpmul  32972  dpmul4  32973  subfacp1lem3  35364  dmcnvep  38709  redvmptabs  42792  cotrclrcl  44169  sqwvfoura  46656  sqwvfourb  46657