Theorem 3eqtr3ri 2653

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

Syntax hints:   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  indif2  3870  dfif5  4102  resdm2  5624  co01  5650  funiunfv  6506  dfdom2  7981  1mhlfehlf  11251  crreczi  12989  rei  13896  bpoly3  14789  bpoly4  14790  cos1bnd  14917  rpnnen2lem3  14945  rpnnen2lem11  14953  m1bits  15162  6gcd4e2  15255  3lcm2e6  15440  karatsuba  15792  karatsubaOLD  15793  ring1  18602  sincos4thpi  24265  sincos6thpi  24267  1cubrlem  24568  cht3  24899  bclbnd  25005  bposlem8  25016  ex-ind-dvds  27318  ip1ilem  27681  mdexchi  29194  disjxpin  29401  xppreima  29449  df1stres  29481  df2ndres  29482  dpmul100  29605  0dp2dp  29617  dpmul  29621  dpmul4  29622  xrge0slmod  29844  cnrrext  30054  ballotth  30599  hgt750lemd  30726  poimirlem3  33412  poimirlem30  33439  mbfposadd  33457  asindmre  33495  areaquad  37802  inductionexd  38453  stoweidlem26  40243  3exp4mod41  41533