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 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 2732

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

This theorem is used by:  indif2  4227  dfif5  4499  resindm  6023  resdm2  6227  co01  6258  funiunfv  7245  dfdom2  8984  crreczi  14292  rei  15243  bpoly3  16144  bpoly4  16145  cos1bnd  16275  rpnnen2lem3  16304  rpnnen2lem11  16312  m1bits  16530  6gcd4e2  16628  3lcm2e6  16823  karatsuba  17175  ring1  20452  sincos4thpi  26751  sincos6thpi  26753  1cubrlem  27078  cht3  27409  bclbnd  27516  bposlem8  27527  ex-ind-dvds  30941  ip1ilem  31307  mdexchi  32816  disjxpin  33061  xppreima  33118  df1stres  33176  df2ndres  33177  dpmul100  33342  0dp2dp  33354  dpmul  33358  dpmul4  33359  xrge0slmod  33788  cos9thpiminplylem5  34296  cnrrext  34520  ballotth  35049  hgt750lemd  35156  poimirlem3  38372  poimirlem30  38399  mbfposadd  38416  asindmre  38452  refrelsredund4  39464  420gcd8e4  42872  4p4e8ALT  43125  2p3e5  43132  2p4e6  43133  2p5e7  43134  2p6e8  43135  2p7e9  43136  3p4e7  43137  3p5e8  43138  3p6e9  43139  sqmid3api  43158  areaquad  44057  inductionexd  44995  stoweidlem26  46854  goldratmolem3  47752  3exp4mod41  48519  tposresg  49804