Theorem 3eqtr3ri 2795

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 2788	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2788	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  indif2  4229  dfif5  4502  resindm  6037  resdm2  6251  co01  6284  coires2  6289  funiunfv  7283  dfdom2  9043  crreczi  14413  rei  15366  bpoly3  16268  bpoly4  16269  cos1bnd  16399  rpnnen2lem3  16428  rpnnen2lem11  16436  m1bits  16654  6gcd4e2  16755  3lcm2e6  16952  karatsuba  17305  ring1  20592  sincos4thpi  26899  sincos6thpi  26901  1cubrlem  27226  cht3  27557  bclbnd  27664  bposlem8  27675  ex-ind-dvds  31119  ip1ilem  31485  mdexchi  32994  disjxpin  33280  xppreima  33337  df1stres  33394  df2ndres  33395  dpmul100  33559  0dp2dp  33571  dpmul  33575  dpmul4  33576  xrge0slmod  34013  cos9thpiminplylem5  34529  cnrrext  34753  ballotth  35281  hgt750lemd  35388  poimirlem3  38809  poimirlem30  38836  mbfposadd  38853  asindmre  38889  refrelsredund4  39914  420gcd8e4  43322  4p4e8ALT  43575  2p3e5  43582  2p4e6  43583  2p5e7  43584  2p6e8  43585  2p7e9  43586  3p4e7  43587  3p5e8  43588  3p6e9  43589  sqmid3api  43606  areaquad  44479  inductionexd  45416  stoweidlem26  47309  goldratmolem3  48207  3exp4mod41  48974  bru3eq  49756  tposresg  50322