Theorem 3eqtr3ri 2762

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 2755	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2755	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  indif2  4247  dfif5  4508  resdm2  6207  co01  6237  funiunfv  7225  dfdom2  8952  crreczi  14200  rei  15129  bpoly3  16031  bpoly4  16032  cos1bnd  16162  rpnnen2lem3  16191  rpnnen2lem11  16199  m1bits  16417  6gcd4e2  16515  3lcm2e6  16709  karatsuba  17061  ring1  20226  sincos4thpi  26429  sincos6thpi  26432  1cubrlem  26758  cht3  27090  bclbnd  27198  bposlem8  27209  ex-ind-dvds  30397  ip1ilem  30762  mdexchi  32271  disjxpin  32524  xppreima  32576  df1stres  32634  df2ndres  32635  dpmul100  32824  0dp2dp  32836  dpmul  32840  dpmul4  32841  xrge0slmod  33326  cos9thpiminplylem5  33783  cnrrext  34007  ballotth  34536  hgt750lemd  34646  poimirlem3  37624  poimirlem30  37651  mbfposadd  37668  asindmre  37704  refrelsredund4  38630  420gcd8e4  42001  sqmid3api  42278  areaquad  43212  inductionexd  44151  stoweidlem26  46031  3exp4mod41  47621  tposresg  48870