Theorem 3eqtr3ri 2761

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  indif2  4240  dfif5  4501  resdm2  6192  co01  6222  funiunfv  7204  dfdom2  8926  crreczi  14169  rei  15098  bpoly3  16000  bpoly4  16001  cos1bnd  16131  rpnnen2lem3  16160  rpnnen2lem11  16168  m1bits  16386  6gcd4e2  16484  3lcm2e6  16678  karatsuba  17030  ring1  20230  sincos4thpi  26455  sincos6thpi  26458  1cubrlem  26784  cht3  27116  bclbnd  27224  bposlem8  27235  ex-ind-dvds  30440  ip1ilem  30805  mdexchi  32314  disjxpin  32567  xppreima  32619  df1stres  32677  df2ndres  32678  dpmul100  32867  0dp2dp  32879  dpmul  32883  dpmul4  32884  xrge0slmod  33312  cos9thpiminplylem5  33769  cnrrext  33993  ballotth  34522  hgt750lemd  34632  poimirlem3  37610  poimirlem30  37637  mbfposadd  37654  asindmre  37690  refrelsredund4  38616  420gcd8e4  41987  sqmid3api  42264  areaquad  43198  inductionexd  44137  stoweidlem26  46017  3exp4mod41  47610  tposresg  48859