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  6231  co01  6262  funiunfv  7250  dfdom2  8998  crreczi  14365  rei  15316  bpoly3  16217  bpoly4  16218  cos1bnd  16348  rpnnen2lem3  16377  rpnnen2lem11  16385  m1bits  16603  6gcd4e2  16704  3lcm2e6  16901  karatsuba  17254  ring1  20534  sincos4thpi  26835  sincos6thpi  26837  1cubrlem  27162  cht3  27493  bclbnd  27600  bposlem8  27611  ex-ind-dvds  31055  ip1ilem  31421  mdexchi  32930  disjxpin  33175  xppreima  33232  df1stres  33290  df2ndres  33291  dpmul100  33456  0dp2dp  33468  dpmul  33472  dpmul4  33473  xrge0slmod  33902  cos9thpiminplylem5  34411  cnrrext  34635  ballotth  35163  hgt750lemd  35270  poimirlem3  38521  poimirlem30  38548  mbfposadd  38565  asindmre  38601  refrelsredund4  39628  420gcd8e4  43036  4p4e8ALT  43289  2p3e5  43296  2p4e6  43297  2p5e7  43298  2p6e8  43299  2p7e9  43300  3p4e7  43301  3p5e8  43302  3p6e9  43303  sqmid3api  43320  areaquad  44202  inductionexd  45140  stoweidlem26  47005  goldratmolem3  47903  3exp4mod41  48670  tposresg  49955