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

Theorem 3eqtr3ri 2467
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 2460 . 2  |-  B  =  C
51, 4eqtr3i 2460 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1653
This theorem is referenced by:  indif2  3586  dfif5  3753  resdm2  5363  co01  5387  funiunfv  5998  dfdom2  7136  1mhlfehlf  10195  crreczi  11509  rei  11966  cos1bnd  12793  rpnnen2lem3  12821  rpnnen2lem11  12829  m1bits  12957  karatsuba  13425  sincos4thpi  20426  sincos6thpi  20428  1cubrlem  20686  cht3  20961  bclbnd  21069  bposlem8  21080  ip1ilem  22332  mdexchi  23843  disjxpin  24033  xppreima  24064  df1stres  24096  df2ndres  24097  ballotth  24800  bpoly3  26109  bpoly4  26110  mbfposadd  26266  stoweidlem26  27765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator