Theorem 3eqtr3ri 2794

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  indif2  4233  dfif5  4497  resindm  6016  resdm2  6218  co01  6249  funiunfv  7232  dfdom2  8959  crreczi  14241  rei  15183  bpoly3  16088  bpoly4  16089  cos1bnd  16219  rpnnen2lem3  16248  rpnnen2lem11  16256  m1bits  16474  6gcd4e2  16572  3lcm2e6  16767  karatsuba  17119  ring1  20356  sincos4thpi  26575  sincos6thpi  26578  1cubrlem  26903  cht3  27234  bclbnd  27341  bposlem8  27352  ex-ind-dvds  30660  ip1ilem  31026  mdexchi  32535  disjxpin  32785  xppreima  32844  df1stres  32903  df2ndres  32904  dpmul100  33071  0dp2dp  33083  dpmul  33087  dpmul4  33088  xrge0slmod  33531  cos9thpiminplylem5  34080  cnrrext  34304  ballotth  34832  hgt750lemd  34939  poimirlem3  38119  poimirlem30  38146  mbfposadd  38163  asindmre  38199  refrelsredund4  39212  420gcd8e4  42620  sqmid3api  42889  areaquad  43790  inductionexd  44728  stoweidlem26  46597  3exp4mod41  48222  tposresg  49496