Theorem 3eqtrri 2849

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

Syntax hints:   = wceq 1533

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 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  dfif5  4482  resindm  5899  difxp1  6021  difxp2  6022  dfdm2  6131  cofunex2g  7650  df1st2  7792  df2nd2  7793  domss2  8675  adderpqlem  10375  dfn2  11909  9p1e10  12099  sqrtm1  14634  0.999...  15236  pockthi  16242  matgsum  21045  indistps  21618  indistps2  21619  refun0  22122  filconn  22490  sincosq3sgn  25085  sincosq4sgn  25086  eff1o  25132  ax5seglem7  26720  0grsubgr  27059  nbupgrres  27145  vtxdginducedm1fi  27325  clwwlknclwwlkdif  27756  cnnvg  28454  cnnvs  28456  cnnvnm  28457  h2hva  28750  h2hsm  28751  h2hnm  28752  hhssva  29033  hhsssm  29034  hhssnm  29035  spansnji  29422  lnopunilem1  29786  lnophmlem2  29793  stadd3i  30024  indifundif  30284  dpmul4  30590  xrsp0  30668  xrsp1  30669  hgt750lemd  31919  hgt750lem  31922  rankeq1o  33632  poimirlem8  34899  mbfposadd  34938  iocunico  39815  corcltrcl  40082  binomcxplemdvsum  40685  cosnegpi  42146  fourierdlem62  42452  fouriersw  42515  salexct3  42624  salgensscntex  42626  caragenuncllem  42793  isomenndlem  42811