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

Theorem 3eqtr3ri 2395
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 2388 . 2  |-  B  =  C
51, 4eqtr3i 2388 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1647
This theorem is referenced by:  indif2  3500  dfif5  3666  resdm2  5266  co01  5290  funiunfv  5895  dfdom2  7030  1mhlfehlf  10083  crreczi  11391  rei  11848  cos1bnd  12675  rpnnen2lem3  12703  rpnnen2lem11  12711  m1bits  12839  karatsuba  13307  sincos4thpi  20099  sincos6thpi  20101  1cubrlem  20359  cht3  20634  bclbnd  20742  bposlem8  20753  ip1ilem  21838  mdexchi  23349  df1stres  23615  df2ndres  23616  coinflippvt  24311  ballotth  24364  bpoly3  25620  bpoly4  25621  stoweidlem26  27366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator