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 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  indif2  4222  dfif5  4484  resdm2  6190  co01  6221  funiunfv  7197  dfdom2  8919  crreczi  14184  rei  15112  bpoly3  16017  bpoly4  16018  cos1bnd  16148  rpnnen2lem3  16177  rpnnen2lem11  16185  m1bits  16403  6gcd4e2  16501  3lcm2e6  16696  karatsuba  17048  ring1  20285  sincos4thpi  26493  sincos6thpi  26496  1cubrlem  26821  cht3  27153  bclbnd  27260  bposlem8  27271  ex-ind-dvds  30549  ip1ilem  30915  mdexchi  32424  disjxpin  32676  xppreima  32736  df1stres  32795  df2ndres  32796  dpmul100  32974  0dp2dp  32986  dpmul  32990  dpmul4  32991  xrge0slmod  33426  cos9thpiminplylem5  33949  cnrrext  34173  ballotth  34701  hgt750lemd  34811  poimirlem3  37961  poimirlem30  37988  mbfposadd  38005  asindmre  38041  refrelsredund4  39054  420gcd8e4  42462  sqmid3api  42732  areaquad  43665  inductionexd  44603  stoweidlem26  46475  3exp4mod41  48094  tposresg  49368