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  4498  resindm  5997  difxp1  6131  difxp2  6132  dfdm2  6247  cofunex2g  7904  df1st2  8050  df2nd2  8051  domss2  9076  adderpqlem  10877  dfn2  12426  9p1e10  12621  sqrtm1  15210  0.999...  15816  pockthi  16847  matgsum  22393  indistps  22967  indistps2  22968  refun0  23471  filconn  23839  sincosq3sgn  26477  sincosq4sgn  26478  eff1o  26526  ax5seglem7  29020  0grsubgr  29363  nbupgrres  29449  vtxdginducedm1fi  29630  clwwlknclwwlkdif  30066  cnnvg  30766  cnnvs  30768  cnnvnm  30769  h2hva  31062  h2hsm  31063  h2hnm  31064  hhssva  31345  hhsssm  31346  hhssnm  31347  spansnji  31734  lnopunilem1  32098  lnophmlem2  32105  stadd3i  32336  indifundif  32611  dpmul4  33006  xrsp0  33105  xrsp1  33106  hgt750lemd  34826  hgt750lem  34829  rankeq1o  36387  poimirlem8  37879  mbfposadd  37918  iocunico  43568  corcltrcl  44095  binomcxplemdvsum  44711  cosnegpi  46225  fourierdlem62  46526  fouriersw  46589  salexct3  46700  salgensscntex  46702  caragenuncllem  46870  isomenndlem  46888  usgrexmpl2edg  48389