Theorem 3eqtr2ri 2790

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  funimacnv  6614  uniqs  8773  ackbij1lem13  10233  ef01bndlem  16272  cos2bnd  16276  divalglem2  16485  lefld  18680  smndex2dlinvh  19029  discmp  23623  unmbl  25765  sinhalfpilem  26701  log2cnv  27181  lgam1  27300  ip0i  31306  polid2i  31638  hh0v  31649  pjinormii  32157  dfdec100  33300  dpmul100  33342  dpmul  33358  dpmul4  33359  subfacp1lem3  35761  dmcnvep  39136  25or6to4  43072  redvmptabs  43235  cotrclrcl  44582  sqwvfoura  47056  sqwvfourb  47057