Theorem 3eqtr3ri 2775

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 2768	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2768	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  indif2  4201  dfif5  4472  resdm2  6123  co01  6154  funiunfv  7103  dfdom2  8721  1mhlfehlf  12122  crreczi  13871  rei  14795  bpoly3  15696  bpoly4  15697  cos1bnd  15824  rpnnen2lem3  15853  rpnnen2lem11  15861  m1bits  16075  6gcd4e2  16174  3lcm2e6  16364  karatsuba  16713  ring1  19756  sincos4thpi  25575  sincos6thpi  25577  1cubrlem  25896  cht3  26227  bclbnd  26333  bposlem8  26344  ex-ind-dvds  28726  ip1ilem  29089  mdexchi  30598  disjxpin  30828  xppreima  30884  df1stres  30938  df2ndres  30939  dpmul100  31073  0dp2dp  31085  dpmul  31089  dpmul4  31090  xrge0slmod  31450  cnrrext  31860  ballotth  32404  hgt750lemd  32528  poimirlem3  35707  poimirlem30  35734  mbfposadd  35751  asindmre  35787  refrelsredund4  36672  420gcd8e4  39942  sqmid3api  40232  areaquad  40963  inductionexd  41654  stoweidlem26  43457  3exp4mod41  44956