Theorem 3eqtr3ri 2771

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

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  indif2  4209  dfif5  4471  resdm2  6182  co01  6213  funiunfv  7192  dfdom2  8915  crreczi  14181  rei  15109  bpoly3  16014  bpoly4  16015  cos1bnd  16145  rpnnen2lem3  16174  rpnnen2lem11  16182  m1bits  16400  6gcd4e2  16498  3lcm2e6  16693  karatsuba  17045  ring1  20282  sincos4thpi  26495  sincos6thpi  26498  1cubrlem  26823  cht3  27154  bclbnd  27261  bposlem8  27272  ex-ind-dvds  30549  ip1ilem  30915  mdexchi  32424  disjxpin  32677  xppreima  32737  df1stres  32796  df2ndres  32797  dpmul100  32975  0dp2dp  32987  dpmul  32991  dpmul4  32992  xrge0slmod  33431  cos9thpiminplylem5  33970  cnrrext  34194  ballotth  34722  hgt750lemd  34832  poimirlem3  37990  poimirlem30  38017  mbfposadd  38034  asindmre  38070  refrelsredund4  39083  420gcd8e4  42491  sqmid3api  42760  areaquad  43661  inductionexd  44599  stoweidlem26  46469  3exp4mod41  48094  tposresg  49368