Theorem 3eqtrri 2788

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  dfif5  4498  resindmOLD  6022  difxp1  6158  difxp2  6159  dfdm2  6287  cofunex2g  7966  df1st2  8115  df2nd2  8116  domss2  9162  adderpqlem  11046  dfn2  12626  9p1e10  12823  sqrtm1  15451  0.999...  16059  pockthi  17094  matgsum  22761  indistps  23338  indistps2  23339  refun0  23843  filconn  24211  sincosq3sgn  26838  sincosq4sgn  26839  eff1o  26886  ax5seglem7  29522  0grsubgr  29868  nbupgrres  29954  vtxdginducedm1fi  30134  clwwlknclwwlkdif  30579  cnnvg  31289  cnnvs  31291  cnnvnm  31292  h2hva  31585  h2hsm  31586  h2hnm  31587  hhssva  31868  hhsssm  31869  hhssnm  31870  spansnji  32257  lnopunilem1  32621  lnophmlem2  32628  stadd3i  32859  indifundif  33171  dpmul4  33530  xrsp0  33623  xrsp1  33624  hgt750lemd  35327  hgt750lem  35330  rankeq1o  37028  poimirlem8  38655  mbfposadd  38694  iocunico  44322  corcltrcl  44848  binomcxplemdvsum  45448  cosnegpi  46985  fourierdlem62  47286  fouriersw  47349  salexct3  47460  salgensscntex  47462  caragenuncllem  47630  isomenndlem  47648  goldpolyfactor  48035  goldratmolem2  48041  usgrexmpl2edg  49235