Theorem 3eqtr3ri 2801

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

Syntax hints:   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  indif2  4242  dfif5  4509  resindm  6030  resdm2  6233  co01  6264  funiunfv  7247  dfdom2  8974  crreczi  14263  rei  15206  bpoly3  16111  bpoly4  16112  cos1bnd  16242  rpnnen2lem3  16271  rpnnen2lem11  16279  m1bits  16497  6gcd4e2  16595  3lcm2e6  16790  karatsuba  17142  ring1  20392  sincos4thpi  26643  sincos6thpi  26646  1cubrlem  26971  cht3  27302  bclbnd  27409  bposlem8  27420  ex-ind-dvds  30752  ip1ilem  31118  mdexchi  32627  disjxpin  32873  xppreima  32930  df1stres  32989  df2ndres  32990  dpmul100  33156  0dp2dp  33168  dpmul  33172  dpmul4  33173  xrge0slmod  33610  cos9thpiminplylem5  34120  cnrrext  34344  ballotth  34872  hgt750lemd  34979  poimirlem3  38161  poimirlem30  38188  mbfposadd  38205  asindmre  38241  refrelsredund4  39254  420gcd8e4  42662  sqmid3api  42933  areaquad  43834  inductionexd  44772  stoweidlem26  46631  3exp4mod41  48256  tposresg  49540