MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3ri Structured version   Visualization version   GIF version

Theorem 3eqtr3ri 2853
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
StepHypRef Expression
1 3eqtr3i.3 . 2 𝐵 = 𝐷
2 3eqtr3i.1 . . 3 𝐴 = 𝐵
3 3eqtr3i.2 . . 3 𝐴 = 𝐶
42, 3eqtr3i 2846 . 2 𝐵 = 𝐶
51, 4eqtr3i 2846 1 𝐷 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814
This theorem is referenced by:  indif2  4222  dfif5  4456  resdm2  6061  co01  6087  funiunfv  6981  dfdom2  8510  1mhlfehlf  11834  crreczi  13573  rei  14494  bpoly3  15391  bpoly4  15392  cos1bnd  15519  rpnnen2lem3  15548  rpnnen2lem11  15556  m1bits  15766  6gcd4e2  15863  3lcm2e6  16049  karatsuba  16397  ring1  19330  sincos4thpi  25084  sincos6thpi  25086  1cubrlem  25405  cht3  25736  bclbnd  25842  bposlem8  25853  ex-ind-dvds  28224  ip1ilem  28587  mdexchi  30096  disjxpin  30324  xppreima  30380  df1stres  30425  df2ndres  30426  dpmul100  30559  0dp2dp  30571  dpmul  30575  dpmul4  30576  xrge0slmod  30924  cnrrext  31258  ballotth  31802  hgt750lemd  31926  poimirlem3  34940  poimirlem30  34967  mbfposadd  34984  asindmre  35020  refrelsredund4  35907  420gcd8e4  39162  sqmid3api  39293  areaquad  39963  inductionexd  40642  stoweidlem26  42461  3exp4mod41  43928
  Copyright terms: Public domain W3C validator