Theorem 3eqtr3ri 2772

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

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  indif2  4287  dfif5  4547  resdm2  6253  co01  6283  funiunfv  7268  dfdom2  9017  1mhlfehlf  12483  crreczi  14264  rei  15192  bpoly3  16091  bpoly4  16092  cos1bnd  16220  rpnnen2lem3  16249  rpnnen2lem11  16257  m1bits  16474  6gcd4e2  16572  3lcm2e6  16766  karatsuba  17118  ring1  20324  sincos4thpi  26570  sincos6thpi  26573  1cubrlem  26899  cht3  27231  bclbnd  27339  bposlem8  27350  ex-ind-dvds  30490  ip1ilem  30855  mdexchi  32364  disjxpin  32608  xppreima  32662  df1stres  32719  df2ndres  32720  dpmul100  32864  0dp2dp  32876  dpmul  32880  dpmul4  32881  xrge0slmod  33356  cnrrext  33973  ballotth  34519  hgt750lemd  34642  poimirlem3  37610  poimirlem30  37637  mbfposadd  37654  asindmre  37690  refrelsredund4  38614  420gcd8e4  41988  sqmid3api  42297  areaquad  43205  inductionexd  44145  stoweidlem26  45982  3exp4mod41  47541