Theorem 3eqtr3ri 2811

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

Syntax hints:   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  indif2  4097  dfif5  4323  resdm2  5880  co01  5906  funiunfv  6780  dfdom2  8269  1mhlfehlf  11606  crreczi  13313  rei  14309  bpoly3  15200  bpoly4  15201  cos1bnd  15328  rpnnen2lem3  15358  rpnnen2lem11  15366  m1bits  15578  6gcd4e2  15671  3lcm2e6  15855  karatsuba  16203  ring1  19000  sincos4thpi  24714  sincos6thpi  24716  1cubrlem  25030  cht3  25362  bclbnd  25468  bposlem8  25479  ex-ind-dvds  27910  ip1ilem  28270  mdexchi  29783  disjxpin  29981  xppreima  30031  df1stres  30064  df2ndres  30065  dpmul100  30181  0dp2dp  30193  dpmul  30197  dpmul4  30198  xrge0slmod  30414  cnrrext  30660  ballotth  31206  hgt750lemd  31336  poimirlem3  34047  poimirlem30  34074  mbfposadd  34091  asindmre  34129  refrelsred4  35010  sqmid3api  38159  areaquad  38774  inductionexd  39423  stoweidlem26  41184  3exp4mod41  42568