Theorem 3eqtr3ri 2763

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 2756	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2756	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  indif2  4228  dfif5  4489  resdm2  6178  co01  6209  funiunfv  7182  dfdom2  8900  crreczi  14135  rei  15063  bpoly3  15965  bpoly4  15966  cos1bnd  16096  rpnnen2lem3  16125  rpnnen2lem11  16133  m1bits  16351  6gcd4e2  16449  3lcm2e6  16643  karatsuba  16995  ring1  20228  sincos4thpi  26449  sincos6thpi  26452  1cubrlem  26778  cht3  27110  bclbnd  27218  bposlem8  27229  ex-ind-dvds  30441  ip1ilem  30806  mdexchi  32315  disjxpin  32568  xppreima  32627  df1stres  32685  df2ndres  32686  dpmul100  32877  0dp2dp  32889  dpmul  32893  dpmul4  32894  xrge0slmod  33313  cos9thpiminplylem5  33799  cnrrext  34023  ballotth  34551  hgt750lemd  34661  poimirlem3  37671  poimirlem30  37698  mbfposadd  37715  asindmre  37751  refrelsredund4  38677  420gcd8e4  42047  sqmid3api  42324  areaquad  43257  inductionexd  44196  stoweidlem26  46072  3exp4mod41  47655  tposresg  48917