Theorem 3eqtr3ri 2793

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  indif2  4227  dfif5  4499  resindm  6019  resdm2  6233  co01  6264  funiunfv  7253  dfdom2  9006  crreczi  14373  rei  15324  bpoly3  16225  bpoly4  16226  cos1bnd  16356  rpnnen2lem3  16385  rpnnen2lem11  16393  m1bits  16611  6gcd4e2  16712  3lcm2e6  16909  karatsuba  17262  ring1  20542  sincos4thpi  26843  sincos6thpi  26845  1cubrlem  27170  cht3  27501  bclbnd  27608  bposlem8  27619  ex-ind-dvds  31063  ip1ilem  31429  mdexchi  32938  disjxpin  33183  xppreima  33240  df1stres  33298  df2ndres  33299  dpmul100  33464  0dp2dp  33476  dpmul  33480  dpmul4  33481  xrge0slmod  33910  cos9thpiminplylem5  34419  cnrrext  34643  ballotth  35171  hgt750lemd  35278  poimirlem3  38543  poimirlem30  38570  mbfposadd  38587  asindmre  38623  refrelsredund4  39650  420gcd8e4  43058  4p4e8ALT  43311  2p3e5  43318  2p4e6  43319  2p5e7  43320  2p6e8  43321  2p7e9  43322  3p4e7  43323  3p5e8  43324  3p6e9  43325  sqmid3api  43342  areaquad  44219  inductionexd  45156  stoweidlem26  47037  goldratmolem3  47935  3exp4mod41  48702  tposresg  49987