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

Theorem 3eqtr3ri 2314
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3ri  |-  D  =  C

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2  |-  B  =  D
2 3eqtr3i.1 . . 3  |-  A  =  B
3 3eqtr3i.2 . . 3  |-  A  =  C
42, 3eqtr3i 2307 . 2  |-  B  =  C
51, 4eqtr3i 2307 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1625
This theorem is referenced by:  indif2  3414  dfif5  3579  resdm2  5165  co01  5189  funiunfv  5776  dfdom2  6889  1mhlfehlf  9936  crreczi  11228  rei  11643  cos1bnd  12469  rpnnen2lem3  12497  rpnnen2lem11  12505  m1bits  12633  karatsuba  13101  sincos4thpi  19883  sincos6thpi  19885  1cubrlem  20139  cht3  20413  bclbnd  20521  bposlem8  20532  ip1ilem  21406  mdexchi  22917  ballotth  23098  df1stres  23245  df2ndres  23246  coinflippvt  23687  bpoly3  24795  bpoly4  24796  cntrset  25613  stoweidlem26  27786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278
  Copyright terms: Public domain W3C validator