Theorem 3eqtr3ri 2768

Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri

Step	Hyp	Ref	Expression
1		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
2		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
4	2, 3	eqtr3i 2761	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2761	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  indif2  4235  dfif5  4507  resdm2  6188  co01  6218  funiunfv  7200  dfdom2  8925  1mhlfehlf  12381  crreczi  14141  rei  15053  bpoly3  15952  bpoly4  15953  cos1bnd  16080  rpnnen2lem3  16109  rpnnen2lem11  16117  m1bits  16331  6gcd4e2  16430  3lcm2e6  16618  karatsuba  16967  ring1  20040  sincos4thpi  25907  sincos6thpi  25909  1cubrlem  26228  cht3  26559  bclbnd  26665  bposlem8  26676  ex-ind-dvds  29468  ip1ilem  29831  mdexchi  31340  disjxpin  31573  xppreima  31629  df1stres  31685  df2ndres  31686  dpmul100  31823  0dp2dp  31835  dpmul  31839  dpmul4  31840  xrge0slmod  32211  cnrrext  32680  ballotth  33226  hgt750lemd  33350  poimirlem3  36154  poimirlem30  36181  mbfposadd  36198  asindmre  36234  refrelsredund4  37167  420gcd8e4  40536  sqmid3api  40855  areaquad  41608  inductionexd  42549  stoweidlem26  44387  3exp4mod41  45928