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 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  indif2  4270  dfif5  4544  resdm2  6230  co01  6260  funiunfv  7249  dfdom2  8976  1mhlfehlf  12433  crreczi  14193  rei  15105  bpoly3  16004  bpoly4  16005  cos1bnd  16132  rpnnen2lem3  16161  rpnnen2lem11  16169  m1bits  16383  6gcd4e2  16482  3lcm2e6  16670  karatsuba  17019  ring1  20126  sincos4thpi  26030  sincos6thpi  26032  1cubrlem  26353  cht3  26684  bclbnd  26790  bposlem8  26801  ex-ind-dvds  29752  ip1ilem  30117  mdexchi  31626  disjxpin  31857  xppreima  31909  df1stres  31963  df2ndres  31964  dpmul100  32101  0dp2dp  32113  dpmul  32117  dpmul4  32118  xrge0slmod  32504  cnrrext  33059  ballotth  33605  hgt750lemd  33729  poimirlem3  36577  poimirlem30  36604  mbfposadd  36621  asindmre  36657  refrelsredund4  37588  420gcd8e4  40957  sqmid3api  41277  areaquad  42047  inductionexd  42988  stoweidlem26  44821  3exp4mod41  46363