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 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  indif2  4234  dfif5  4504  resindm  6029  resdm2  6232  co01  6263  funiunfv  7246  dfdom2  8971  crreczi  14260  rei  15203  bpoly3  16107  bpoly4  16108  cos1bnd  16238  rpnnen2lem3  16267  rpnnen2lem11  16275  m1bits  16493  6gcd4e2  16591  3lcm2e6  16786  karatsuba  17138  ring1  20389  sincos4thpi  26678  sincos6thpi  26681  1cubrlem  27006  cht3  27337  bclbnd  27444  bposlem8  27455  ex-ind-dvds  30812  ip1ilem  31178  mdexchi  32687  disjxpin  32933  xppreima  32990  df1stres  33049  df2ndres  33050  dpmul100  33216  0dp2dp  33228  dpmul  33232  dpmul4  33233  xrge0slmod  33668  cos9thpiminplylem5  34176  cnrrext  34400  ballotth  34928  hgt750lemd  35035  poimirlem3  38274  poimirlem30  38301  mbfposadd  38318  asindmre  38354  refrelsredund4  39365  420gcd8e4  42773  sqmid3api  43044  areaquad  43943  inductionexd  44881  stoweidlem26  46740  3exp4mod41  48368  tposresg  49656