Theorem 3eqtr3ri 2774

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

Syntax hints:   = wceq 1540

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  indif2  4281  dfif5  4542  resdm2  6251  co01  6281  funiunfv  7268  dfdom2  9018  1mhlfehlf  12485  crreczi  14267  rei  15195  bpoly3  16094  bpoly4  16095  cos1bnd  16223  rpnnen2lem3  16252  rpnnen2lem11  16260  m1bits  16477  6gcd4e2  16575  3lcm2e6  16769  karatsuba  17121  ring1  20307  sincos4thpi  26555  sincos6thpi  26558  1cubrlem  26884  cht3  27216  bclbnd  27324  bposlem8  27335  ex-ind-dvds  30480  ip1ilem  30845  mdexchi  32354  disjxpin  32601  xppreima  32655  df1stres  32713  df2ndres  32714  dpmul100  32879  0dp2dp  32891  dpmul  32895  dpmul4  32896  xrge0slmod  33376  cnrrext  34011  ballotth  34540  hgt750lemd  34663  poimirlem3  37630  poimirlem30  37657  mbfposadd  37674  asindmre  37710  refrelsredund4  38633  420gcd8e4  42007  sqmid3api  42318  areaquad  43228  inductionexd  44168  stoweidlem26  46041  3exp4mod41  47603  tposresg  48778