Theorem 3eqtrri 2649

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	|- A = B
3eqtri.2	|- B = C
3eqtri.3	|- C = D

Assertion

Ref	Expression
3eqtrri	|- D = A

Proof of Theorem 3eqtrri

Step	Hyp	Ref	Expression
1		3eqtri.1	. . 3 |- A = B
2		3eqtri.2	. . 3 |- B = C
3	1, 2	eqtri 2644	. 2 |- A = C
4		3eqtri.3	. 2 |- C = D
5	3, 4	eqtr2i 2645	1 |- D = A

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  dfif5  4102  resindm  5444  difxp1  5559  difxp2  5560  dfdm2  5667  cofunex2g  7131  df1st2  7263  df2nd2  7264  domss2  8119  adderpqlem  9776  dfn2  11305  9p1e10  11496  sq10OLD  13051  sqrtm1  14016  0.999...  14612  0.999...OLD  14613  pockthi  15611  matgsum  20243  indistps  20815  indistps2  20816  refun0  21318  filconn  21687  sincosq3sgn  24252  sincosq4sgn  24253  eff1o  24295  ax5seglem7  25815  0grsubgr  26170  nbupgrres  26266  vtxdginducedm1fi  26440  clwwlknclwwlkdifs  26873  cnnvg  27533  cnnvs  27535  cnnvnm  27536  h2hva  27831  h2hsm  27832  h2hnm  27833  hhssva  28114  hhsssm  28115  hhssnm  28116  spansnji  28505  lnopunilem1  28869  lnophmlem2  28876  stadd3i  29107  indifundif  29356  dpmul4  29622  xrsp0  29681  xrsp1  29682  hgt750lemd  30726  hgt750lem  30729  rankeq1o  32278  poimirlem8  33417  mbfposadd  33457  iocunico  37796  corcltrcl  38031  binomcxplemdvsum  38554  cosnegpi  40078  fourierdlem62  40385  fouriersw  40448  salexct3  40560  salgensscntex  40562  caragenuncllem  40726  isomenndlem  40744