Theorem 3eqtr3ri 2769

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

Syntax hints:   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  indif2  4235  dfif5  4498  resdm2  6197  co01  6228  funiunfv  7204  dfdom2  8927  crreczi  14163  rei  15091  bpoly3  15993  bpoly4  15994  cos1bnd  16124  rpnnen2lem3  16153  rpnnen2lem11  16161  m1bits  16379  6gcd4e2  16477  3lcm2e6  16671  karatsuba  17023  ring1  20257  sincos4thpi  26490  sincos6thpi  26493  1cubrlem  26819  cht3  27151  bclbnd  27259  bposlem8  27270  ex-ind-dvds  30548  ip1ilem  30914  mdexchi  32423  disjxpin  32675  xppreima  32735  df1stres  32794  df2ndres  32795  dpmul100  32989  0dp2dp  33001  dpmul  33005  dpmul4  33006  xrge0slmod  33441  cos9thpiminplylem5  33964  cnrrext  34188  ballotth  34716  hgt750lemd  34826  poimirlem3  37874  poimirlem30  37901  mbfposadd  37918  asindmre  37954  refrelsredund4  38967  420gcd8e4  42376  sqmid3api  42653  areaquad  43573  inductionexd  44511  stoweidlem26  46384  3exp4mod41  47976  tposresg  49237