Theorem 3eqtr3ri 2792

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

This proof depends on syntax axioms:   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  indif2  4225  dfif5  4498  resindm  6021  resdm2  6235  co01  6266  funiunfv  7256  dfdom2  9013  crreczi  14379  rei  15332  bpoly3  16233  bpoly4  16234  cos1bnd  16364  rpnnen2lem3  16393  rpnnen2lem11  16401  m1bits  16619  6gcd4e2  16720  3lcm2e6  16917  karatsuba  17270  ring1  20550  sincos4thpi  26851  sincos6thpi  26853  1cubrlem  27178  cht3  27509  bclbnd  27616  bposlem8  27627  ex-ind-dvds  31071  ip1ilem  31437  mdexchi  32946  disjxpin  33233  xppreima  33290  df1stres  33348  df2ndres  33349  dpmul100  33513  0dp2dp  33525  dpmul  33529  dpmul4  33530  xrge0slmod  33959  cos9thpiminplylem5  34468  cnrrext  34692  ballotth  35220  hgt750lemd  35327  poimirlem3  38678  poimirlem30  38705  mbfposadd  38722  asindmre  38758  refrelsredund4  39785  420gcd8e4  43193  4p4e8ALT  43446  2p3e5  43453  2p4e6  43454  2p5e7  43455  2p6e8  43456  2p7e9  43457  3p4e7  43458  3p5e8  43459  3p6e9  43460  sqmid3api  43477  areaquad  44355  inductionexd  45292  stoweidlem26  47172  goldratmolem3  48070  3exp4mod41  48837  tposresg  50127