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  20195  sincos4thpi  26398  sincos6thpi  26401  1cubrlem  26727  cht3  27059  bclbnd  27167  bposlem8  27178  ex-ind-dvds  30363  ip1ilem  30728  mdexchi  32237  disjxpin  32490  xppreima  32542  df1stres  32600  df2ndres  32601  dpmul100  32790  0dp2dp  32802  dpmul  32806  dpmul4  32807  xrge0slmod  33292  cos9thpiminplylem5  33749  cnrrext  33973  ballotth  34502  hgt750lemd  34612  poimirlem3  37590  poimirlem30  37617  mbfposadd  37634  asindmre  37670  refrelsredund4  38596  420gcd8e4  41967  sqmid3api  42244  areaquad  43178  inductionexd  44117  stoweidlem26  45997  3exp4mod41  47590  tposresg  48839