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

Theorem 3eqtr3ri 2312
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 2305 . 2  |-  B  =  C
51, 4eqtr3i 2305 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  indif2  3412  dfif5  3577  resdm2  5163  co01  5187  funiunfv  5774  dfdom2  6887  1mhlfehlf  9934  crreczi  11226  rei  11641  cos1bnd  12467  rpnnen2lem3  12495  rpnnen2lem11  12503  m1bits  12631  karatsuba  13099  sincos4thpi  19881  sincos6thpi  19883  1cubrlem  20137  cht3  20411  bclbnd  20519  bposlem8  20530  ip1ilem  21404  mdexchi  22915  ballotth  23096  df1stres  23243  df2ndres  23244  coinflippvt  23685  bpoly3  24793  bpoly4  24794  cntrset  25602  stoweidlem26  27775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator