Theorem 3eqtr3ri 2791

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

Syntax hints:   = wceq 1632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  indif2  4013  dfif5  4246  resdm2  5785  co01  5811  funiunfv  6669  dfdom2  8147  1mhlfehlf  11443  crreczi  13183  rei  14095  bpoly3  14988  bpoly4  14989  cos1bnd  15116  rpnnen2lem3  15144  rpnnen2lem11  15152  m1bits  15364  6gcd4e2  15457  3lcm2e6  15642  karatsuba  15994  karatsubaOLD  15995  ring1  18802  sincos4thpi  24464  sincos6thpi  24466  1cubrlem  24767  cht3  25098  bclbnd  25204  bposlem8  25215  ex-ind-dvds  27629  ip1ilem  27990  mdexchi  29503  disjxpin  29708  xppreima  29758  df1stres  29790  df2ndres  29791  dpmul100  29914  0dp2dp  29926  dpmul  29930  dpmul4  29931  xrge0slmod  30153  cnrrext  30363  ballotth  30908  hgt750lemd  31035  poimirlem3  33725  poimirlem30  33752  mbfposadd  33770  asindmre  33808  areaquad  38304  inductionexd  38955  stoweidlem26  40746  3exp4mod41  42043