Theorem 3eqtr2ri 2799

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  funimacnv  6618  uniqs  8770  ackbij1lem13  10213  ef01bndlem  16239  cos2bnd  16243  divalglem2  16452  lefld  18647  smndex2dlinvh  18978  discmp  23523  unmbl  25664  sinhalfpilem  26593  log2cnv  27074  lgam1  27193  ip0i  31117  polid2i  31449  hh0v  31460  pjinormii  31968  dfdec100  33114  dpmul100  33156  dpmul  33172  dpmul4  33173  subfacp1lem3  35572  dmcnvep  38926  25or6to4  42862  redvmptabs  43010  cotrclrcl  44359  sqwvfoura  46833  sqwvfourb  46834