Theorem 3eqtrri 2762

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  dfif5  4494  resindm  5987  difxp1  6121  difxp2  6122  dfdm2  6237  cofunex2g  7892  df1st2  8038  df2nd2  8039  domss2  9062  adderpqlem  10863  dfn2  12412  9p1e10  12607  sqrtm1  15196  0.999...  15802  pockthi  16833  matgsum  22379  indistps  22953  indistps2  22954  refun0  23457  filconn  23825  sincosq3sgn  26463  sincosq4sgn  26464  eff1o  26512  ax5seglem7  28957  0grsubgr  29300  nbupgrres  29386  vtxdginducedm1fi  29567  clwwlknclwwlkdif  30003  cnnvg  30702  cnnvs  30704  cnnvnm  30705  h2hva  30998  h2hsm  30999  h2hnm  31000  hhssva  31281  hhsssm  31282  hhssnm  31283  spansnji  31670  lnopunilem1  32034  lnophmlem2  32041  stadd3i  32272  indifundif  32548  dpmul4  32944  xrsp0  33043  xrsp1  33044  hgt750lemd  34754  hgt750lem  34757  rankeq1o  36314  poimirlem8  37768  mbfposadd  37807  iocunico  43395  corcltrcl  43922  binomcxplemdvsum  44538  cosnegpi  46053  fourierdlem62  46354  fouriersw  46417  salexct3  46528  salgensscntex  46530  caragenuncllem  46698  isomenndlem  46716  usgrexmpl2edg  48217