Theorem 3eqtrri 2773

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtri.1	⊢ 𝐴 = 𝐵
3eqtri.2	⊢ 𝐵 = 𝐶
3eqtri.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtrri	⊢ 𝐷 = 𝐴

Proof of Theorem 3eqtrri

Step	Hyp	Ref	Expression
1		3eqtri.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtri 2768	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2769	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  dfif5  4564  resindm  6059  difxp1  6196  difxp2  6197  dfdm2  6312  cofunex2g  7990  df1st2  8139  df2nd2  8140  domss2  9202  adderpqlem  11023  dfn2  12566  9p1e10  12760  sqrtm1  15324  0.999...  15929  pockthi  16954  matgsum  22464  indistps  23039  indistps2  23040  refun0  23544  filconn  23912  sincosq3sgn  26560  sincosq4sgn  26561  eff1o  26609  ax5seglem7  28968  0grsubgr  29313  nbupgrres  29399  vtxdginducedm1fi  29580  clwwlknclwwlkdif  30011  cnnvg  30710  cnnvs  30712  cnnvnm  30713  h2hva  31006  h2hsm  31007  h2hnm  31008  hhssva  31289  hhsssm  31290  hhssnm  31291  spansnji  31678  lnopunilem1  32042  lnophmlem2  32049  stadd3i  32280  indifundif  32554  dpmul4  32878  xrsp0  32995  xrsp1  32996  hgt750lemd  34625  hgt750lem  34628  rankeq1o  36135  poimirlem8  37588  mbfposadd  37627  iocunico  43172  corcltrcl  43701  binomcxplemdvsum  44324  cosnegpi  45788  fourierdlem62  46089  fouriersw  46152  salexct3  46263  salgensscntex  46265  caragenuncllem  46433  isomenndlem  46451  usgrexmpl2edg  47844