Theorem 3eqtrri 2768

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 2763	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2764	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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  dfif5  4547  resindm  6050  difxp1  6187  difxp2  6188  dfdm2  6303  cofunex2g  7973  df1st2  8122  df2nd2  8123  domss2  9175  adderpqlem  10992  dfn2  12537  9p1e10  12733  sqrtm1  15311  0.999...  15914  pockthi  16941  matgsum  22459  indistps  23034  indistps2  23035  refun0  23539  filconn  23907  sincosq3sgn  26557  sincosq4sgn  26558  eff1o  26606  ax5seglem7  28965  0grsubgr  29310  nbupgrres  29396  vtxdginducedm1fi  29577  clwwlknclwwlkdif  30008  cnnvg  30707  cnnvs  30709  cnnvnm  30710  h2hva  31003  h2hsm  31004  h2hnm  31005  hhssva  31286  hhsssm  31287  hhssnm  31288  spansnji  31675  lnopunilem1  32039  lnophmlem2  32046  stadd3i  32277  indifundif  32552  dpmul4  32881  xrsp0  32997  xrsp1  32998  hgt750lemd  34642  hgt750lem  34645  rankeq1o  36153  poimirlem8  37615  mbfposadd  37654  iocunico  43200  corcltrcl  43729  binomcxplemdvsum  44351  cosnegpi  45823  fourierdlem62  46124  fouriersw  46187  salexct3  46298  salgensscntex  46300  caragenuncllem  46468  isomenndlem  46486  usgrexmpl2edg  47924