Theorem 3eqtrri 2678

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

Syntax hints:   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  dfif5  4135  resindm  5479  difxp1  5594  difxp2  5595  dfdm2  5705  cofunex2g  7173  df1st2  7308  df2nd2  7309  domss2  8160  adderpqlem  9814  dfn2  11343  9p1e10  11534  sq10OLD  13091  sqrtm1  14060  0.999...  14656  0.999...OLD  14657  pockthi  15658  matgsum  20291  indistps  20863  indistps2  20864  refun0  21366  filconn  21734  sincosq3sgn  24297  sincosq4sgn  24298  eff1o  24340  ax5seglem7  25860  0grsubgr  26215  nbupgrres  26310  vtxdginducedm1fi  26496  clwwlknclwwlkdif  26945  clwwlknclwwlkdifsOLD  26947  cnnvg  27661  cnnvs  27663  cnnvnm  27664  h2hva  27959  h2hsm  27960  h2hnm  27961  hhssva  28242  hhsssm  28243  hhssnm  28244  spansnji  28633  lnopunilem1  28997  lnophmlem2  29004  stadd3i  29235  indifundif  29482  dpmul4  29750  xrsp0  29809  xrsp1  29810  hgt750lemd  30854  hgt750lem  30857  rankeq1o  32403  poimirlem8  33547  mbfposadd  33587  iocunico  38113  corcltrcl  38348  binomcxplemdvsum  38871  cosnegpi  40396  fourierdlem62  40703  fouriersw  40766  salexct3  40878  salgensscntex  40880  caragenuncllem  41047  isomenndlem  41065