Theorem 3eqtrri 2797

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  dfif5  4509  resindmOLD  6031  difxp1  6163  difxp2  6164  dfdm2  6283  cofunex2g  7946  df1st2  8092  df2nd2  8093  domss2  9123  adderpqlem  10938  dfn2  12516  9p1e10  12712  sqrtm1  15325  0.999...  15934  pockthi  16966  matgsum  22562  indistps  23136  indistps2  23137  refun0  23640  filconn  24008  sincosq3sgn  26630  sincosq4sgn  26631  eff1o  26679  ax5seglem7  29225  0grsubgr  29568  nbupgrres  29654  vtxdginducedm1fi  29834  clwwlknclwwlkdif  30270  cnnvg  30970  cnnvs  30972  cnnvnm  30973  h2hva  31266  h2hsm  31267  h2hnm  31268  hhssva  31549  hhsssm  31550  hhssnm  31551  spansnji  31938  lnopunilem1  32302  lnophmlem2  32309  stadd3i  32540  indifundif  32810  dpmul4  33173  xrsp0  33272  xrsp1  33273  hgt750lemd  34979  hgt750lem  34982  rankeq1o  36561  poimirlem8  38166  mbfposadd  38205  iocunico  43829  corcltrcl  44356  binomcxplemdvsum  44956  cosnegpi  46472  fourierdlem62  46773  fouriersw  46836  salexct3  46947  salgensscntex  46949  caragenuncllem  47117  isomenndlem  47135  goldratmolem2  47511  usgrexmpl2edg  48682