Theorem 3eqtr3ri 2767

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 2760	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2760	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  indif2  4269  dfif5  4543  resdm2  6229  co01  6259  funiunfv  7249  dfdom2  8976  1mhlfehlf  12435  crreczi  14195  rei  15107  bpoly3  16006  bpoly4  16007  cos1bnd  16134  rpnnen2lem3  16163  rpnnen2lem11  16171  m1bits  16385  6gcd4e2  16484  3lcm2e6  16672  karatsuba  17021  ring1  20198  sincos4thpi  26259  sincos6thpi  26261  1cubrlem  26582  cht3  26913  bclbnd  27019  bposlem8  27030  ex-ind-dvds  29981  ip1ilem  30346  mdexchi  31855  disjxpin  32086  xppreima  32138  df1stres  32192  df2ndres  32193  dpmul100  32330  0dp2dp  32342  dpmul  32346  dpmul4  32347  xrge0slmod  32733  cnrrext  33288  ballotth  33834  hgt750lemd  33958  poimirlem3  36794  poimirlem30  36821  mbfposadd  36838  asindmre  36874  refrelsredund4  37805  420gcd8e4  41177  sqmid3api  41497  areaquad  42267  inductionexd  43208  stoweidlem26  45040  3exp4mod41  46582