Theorem 3eqtrri 2765

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

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

This theorem is referenced by:  dfif5  4484  resindm  5990  difxp1  6124  difxp2  6125  dfdm2  6240  cofunex2g  7897  df1st2  8042  df2nd2  8043  domss2  9068  adderpqlem  10871  dfn2  12444  9p1e10  12640  sqrtm1  15231  0.999...  15840  pockthi  16872  matgsum  22415  indistps  22989  indistps2  22990  refun0  23493  filconn  23861  sincosq3sgn  26480  sincosq4sgn  26481  eff1o  26529  ax5seglem7  29021  0grsubgr  29364  nbupgrres  29450  vtxdginducedm1fi  29631  clwwlknclwwlkdif  30067  cnnvg  30767  cnnvs  30769  cnnvnm  30770  h2hva  31063  h2hsm  31064  h2hnm  31065  hhssva  31346  hhsssm  31347  hhssnm  31348  spansnji  31735  lnopunilem1  32099  lnophmlem2  32106  stadd3i  32337  indifundif  32612  dpmul4  32991  xrsp0  33090  xrsp1  33091  hgt750lemd  34811  hgt750lem  34814  rankeq1o  36372  poimirlem8  37966  mbfposadd  38005  iocunico  43660  corcltrcl  44187  binomcxplemdvsum  44803  cosnegpi  46316  fourierdlem62  46617  fouriersw  46680  salexct3  46791  salgensscntex  46793  caragenuncllem  46961  isomenndlem  46979  usgrexmpl2edg  48520