Theorem 3eqtr3ri 2777

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 2770	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2770	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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  indif2  4300  dfif5  4564  resdm2  6262  co01  6292  funiunfv  7285  dfdom2  9038  1mhlfehlf  12512  crreczi  14277  rei  15205  bpoly3  16106  bpoly4  16107  cos1bnd  16235  rpnnen2lem3  16264  rpnnen2lem11  16272  m1bits  16486  6gcd4e2  16585  3lcm2e6  16779  karatsuba  17131  ring1  20333  sincos4thpi  26573  sincos6thpi  26576  1cubrlem  26902  cht3  27234  bclbnd  27342  bposlem8  27353  ex-ind-dvds  30493  ip1ilem  30858  mdexchi  32367  disjxpin  32610  xppreima  32664  df1stres  32715  df2ndres  32716  dpmul100  32861  0dp2dp  32873  dpmul  32877  dpmul4  32878  xrge0slmod  33341  cnrrext  33956  ballotth  34502  hgt750lemd  34625  poimirlem3  37583  poimirlem30  37610  mbfposadd  37627  asindmre  37663  refrelsredund4  38588  420gcd8e4  41963  sqmid3api  42272  areaquad  43177  inductionexd  44117  stoweidlem26  45947  3exp4mod41  47490