Theorem 3eqtr2ri 2772

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

Syntax hints:   = wceq 1540

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  funimacnv  6647  uniqs  8817  ackbij1lem13  10271  ef01bndlem  16220  cos2bnd  16224  divalglem2  16432  lefld  18637  smndex2dlinvh  18930  discmp  23406  unmbl  25572  sinhalfpilem  26505  log2cnv  26987  lgam1  27107  ip0i  30844  polid2i  31176  hh0v  31187  pjinormii  31695  dfdec100  32832  dpmul100  32879  dpmul  32895  dpmul4  32896  subfacp1lem3  35187  uniqsALTV  38330  redvmptabs  42390  cotrclrcl  43755  sqwvfoura  46243  sqwvfourb  46244